inv.ctt

module inv where

Path (A : U) (a b : A) : U = PathP (<_> A) a b

inv1 (A : U) (a b : A) (p : Path A a b) : Path A b a =
  <i> p @ -i

inv2 (A : U) (a b : A) (p : Path A a b) : Path A b a =
  <i> comp (<_> A) a [(i = 0) -> p, (i = 1) -> <_> a]

inv1Idp (A : U) (a : A) : Path A a a =
  inv1 A a a (<_> a)

inv2Idp (A : U) (a : A) : Path A a a =
  inv2 A a a (<_> a)

{-
> :n inv1Idp
NORMEVAL: \(A : U) -> \(a : A) -> <!0> a
> :n inv2Idp
NORMEVAL: \(A : U) -> \(a : A) -> <!0> comp (<!1> A) a [ (!0 = 0) -> <!1> a, (!0 = 1) -> <!1> a ]
-}

inv2inv2 (A : U) (a b : A) (p : Path A a b) : Path A a b =
  inv2 A b a (inv2 A a b p)