Advertisement
Not a member of Pastebin yet?
Sign Up,
it unlocks many cool features!
- -- H-levels
- isProp (A : U) : U = (x y : A) -> Path A x y
- isSet (A : U) : U = (x y : A) -> isProp (Path A x y)
- propSet (A : U) (h : isProp A) : isSet A = undefined
Advertisement
Add Comment
Please, Sign In to add comment
Advertisement
