Advertisement
Not a member of Pastebin yet?
Sign Up,
it unlocks many cool features!
- module cheery where
- bot : U = (A : U) -> A
- pf (A : U) (x y : A -> bot) : PathP (<_> A -> bot) x y =
- <i> \(a : A) -> x a (PathP (<_> bot) (x a) (y a)) @ i
Advertisement
Add Comment
Please, Sign In to add comment
Advertisement
