propset

Propset package contains basic theorems about Contractible Signletons, Mere Propositions and Set types.

isContr (A: U): U = (x: A) * ((y: A) -> Path A x y) isProp (A: U): U = n_grpd A Z isSet (A: U): U = n_grpd A (S Z)

Theorems

propSig

propSig (A: U) (B: A -> U) (pi1: isProp A) (pi2: (x : A) -> isProp (B x)) (f g: Sigma A B): Path (Sigma A B) f g

propPi

propPi (A: U) (B : A -> U) (h: (x : A) -> isProp (B x)) (f g: Pi A B): Path (Pi A B) f g

propSet

propSet (A: U) (h: isProp A): isSet A