primitives.txt

_=_ : Π {α : U}, α → α → U
idp : Π {α : U} (a : α), a = a
_⁻¹ : Π {α : U} {a b : α}, a = b → b = a
_⬝_ : Π {α : U} {a b c : α}, a = b → b = c → a = c

(p ⬝ q) ⬝ r   ~> p ⬝ (q ⬝ r)
(p ⬝ q)⁻¹     ~> q⁻¹ ⬝ p⁻¹
p ⬝ (p⁻¹ ⬝ q) ~> q
p⁻¹ ⬝ (p ⬝ q) ~> q
p ⬝ p⁻¹       ~> idp a
p⁻¹ ⬝ p       ~> idp b
(p⁻¹)⁻¹       ~> p
(idp x)⁻¹     ~> idp x
p ⬝ idp b     ~> p
idp a ⬝ p     ~> p

coe : Π {A B : U} : A = B → A → B
apd : Π {A : U} {B : A → U} {a b : A} (f : Π (x : A), B x) (p : a = b), coe (apd B p) (f a) = f b

       cong f p⁻¹ ~> (cong f p)⁻¹
   cong f (p ⬝ q) ~> cong f p ⬝ cong f q
cong g (cong f p) ~> cong (g ∘ f) p
        cong id p ~> p
  cong (λ _, x) p ~> idp x
   cong f (idp x) ~> idp (f x)

    N : U
 zero : N
 succ : N → N
N-ind : Π (A : N → V), A zero → (Π n, A n → A (succ n)) → Π n, A n

    N-ind A z s zero ~> z
N-ind A z s (succ n) ~> s n (N-ind A z s n)

    Z : U
  pos : N → Z
  neg : N → Z
Z-ind : Π (A : Z → V), (Π n, A (pos n)) → (Π n, A (neg n)) → Π z, A z

Z-ind A p n (pos x) ~> p x
Z-ind A p n (neg x) ~> n x

Z-succ : Z → Z
Z-pred : Z → Z

Z-succ (neg (succ n)) ~> neg n
    Z-succ (neg zero) ~> pos zero
       Z-succ (pos n) ~> pos (succ n)

       Z-pred (neg n) ~> neg (succ n)
    Z-pred (pos zero) ~> neg zero
Z-pred (pos (succ n)) ~> pos n

Z-succ (Z-pred z) ~> z
Z-pred (Z-succ z) ~> z

    S¹ : U
  base : S¹
  loop : Path S¹ base base
S¹-ind : Π (A : S¹ → U) (b : A base), Path (A base) (coe (cong A loop) b) b → Π (x : S¹), A x

                S¹-ind A b ℓ base ~> b
???
cong (λ x, S¹-ind A b ℓ x) loop ~> ℓ[x/base] ⬝ cong (λ x′ H′, b[x/x′]) loop

     R : U
  elem : Z → R
  glue : Π (z : Z), Path R (elem z) (elem (Z-succ z))
 R-ind : Π (A : R → U) (cz : Π z, A (elem z)), (Π z, Path (A (elem (Z-succ z))) (coe (cong A (glue z)) (cz z)) (cz (Z-succ z))) → Π z, A z
R-inj : Π (x y : Z), Id R (elem x) (elem y) → Id Z x y

              R-ind A cz sz (elem z) ~> cz z
cong (λ x H, R-ind A cz sz) (glue z) ~> sz z
           R-inj x x (refl (elem x)) ~> refl x