FUNEXT

From the categorical point of view functioncal extensionality validates full universal property in LCCC in contrast to weak one.

Constructors

funext (A B: U) (f g: A -> B)
       (p: (x:A) -> Path B (f x) (g x))
     : Path (A -> B) f g

happly (A B: U) (f g: A -> B) (p: Path (A -> B) f g) (x: A)
     : Path B (f x) (g x)

funext_Beta (A B: U) (f g: A -> B)
            (p: (x:A) -> Path B (f x) (g x))
          : (x:A) -> Path B (f x) (g x)

funext_Eta (A B: U) (f g: A -> B)
           (p: Path (A -> B) f g)
         : Path (Path (A -> B) f g) (funext A B f g (happly A B f g p)) p

piext (A: U) (B: A -> U) (f g: (x: A) -> B x)
      (p: (x: A) -> Path (B x) (f x) (g x))
    : Path ((y: A) -> B y) f g