hoq-0.2: examples/Paths.hoq

infixr 5 $
($) : {A B : Type} -> (A -> B) -> A -> B
($) _ _ f a = f a

idp : {A : Type} {a : A} -> a = a
idp _ a = path (\_ -> a)

transport : {A : Type} (B : A -> Type) {a a' : A} -> a = a' -> B a -> B a'
transport _ B _ _ p x = coe (\i -> B (p @ i)) left x right

psqueeze : {A : Type} {a a' : A} (p : a = a') (i : I) -> a = p @ i
psqueeze _ _ _ p i = path (\j -> p @ squeeze i j)

J : {A : Type} {a : A} (B : {a' : A} -> a = a' -> Type) -> B idp -> {a' : A} (p : a = a') -> B p
J A a B b a' p = coe (\i -> B (psqueeze p i)) left b right

inv : {A : Type} {a a' : A} -> a = a' -> a' = a
inv _ a _ p = transport (\x -> x = a) p idp

(*) : {A : Type} {a a' a'' : A} -> a = a' -> a' = a'' -> a = a''
(*) _ a _ _ p q = transport (\x -> a = x) q p

inv-comp : {A : Type} {a a' : A} (p : a = a') -> inv p * p = idp
inv-comp _ _ _ p = J (\_ q -> inv q * q = idp) idp p

data QED = qed

(!) : {A : Type} -> (a : A) -> QED -> a = a
(!) _ _ _ = idp

infix 3 ==<
(==<) : {A : Type} (a : A) {a' : A} -> a = a' -> a = a'
(==<) _ _ _ p = p

infixr 2 >==
(>==) : {A : Type} {a a' a'' : A} -> a = a' -> a' = a'' -> a = a''
(>==) _ _ _ _ = (*)