Lemma. HoTT 2.1.4 [violet-EVW3]

2026-06-19 · Lîm Tsú-thuàn 
\import std/id

\universe 𝓤S 𝓤

\operator "\x ⋅ \y" => trans x y
  \associativity: \left

Unit laws [local-0]

\let trans-refl-l{A : universe 𝓤} -> {x : A} -> {y : A} -> (p : x = y) -> (refl ⋅ p) = p (i.e. {A : universe 𝓤} -> {x : A} -> {y : A} -> (p : Id x y) -> Id (trans refl p) p) {Auniverse 𝓤 : 𝓤universe S 𝓤} {xA yA : Auniverse 𝓤} (px = y (i.e. Id x y) : xA = yA) : (refl ⋅ p{A : universe 𝓤} -> {x : A} -> {y : A} -> {z : A} -> (_ : x = y) -> (_ : y = z) -> x = z (i.e. {A : universe 𝓤} -> {x : A} -> {y : A} -> {z : A} -> (_ : Id x y) -> (_ : Id y z) -> Id x z)) = px = y (i.e. Id x y) => refl
\let trans-refl-r{A : universe 𝓤} -> {x : A} -> {y : A} -> (p : x = y) -> (p ⋅ refl) = p (i.e. {A : universe 𝓤} -> {x : A} -> {y : A} -> (p : Id x y) -> Id (trans p refl) p) {Auniverse 𝓤 : 𝓤universe S 𝓤} {xA yA : Auniverse 𝓤} : (px = y (i.e. Id x y) : xA = yA) -> (px = i (i.e. Id x i) ⋅ refl) = px = i (i.e. Id x i) \where
  trans-refl-r px = y (i.e. Id x y) <= \elim p$-2 = $-3 (i.e. Id $-2 $-3)
  | trans-refl-r{A : universe 𝓤} -> {x : A} -> {y : A} -> (p : x = y) -> (p ⋅ refl) = p (i.e. {A : universe 𝓤} -> {x : A} -> {y : A} -> (p : Id x y) -> Id (trans p refl) p) refl{A : universe 𝓤} -> {x : A} -> x = x (i.e. {A : universe 𝓤} -> {x : A} -> Id x x) => refl{A : universe 𝓤} -> {x : A} -> x = x (i.e. {A : universe 𝓤} -> {x : A} -> Id x x)

Inverse laws [local-1]

\let trans-sym-l{A : universe 𝓤} -> {x : A} -> {y : A} -> (p : x = y) -> ((sym p) ⋅ p) = refl (i.e. {A : universe 𝓤} -> {x : A} -> {y : A} -> (p : Id x y) -> Id (trans (sym p) p) refl) {Auniverse 𝓤 : 𝓤universe S 𝓤} {xA yA : Auniverse 𝓤} : (px = y (i.e. Id x y) : xA = yA) -> ((sym{A : universe 𝓤} -> {x : A} -> {y : A} -> (_ : x = y) -> y = x (i.e. {A : universe 𝓤} -> {x : A} -> {y : A} -> (_ : Id x y) -> Id y x) px = i (i.e. Id x i)) ⋅ px = i (i.e. Id x i)) = refl \where
  trans-sym-l px = y (i.e. Id x y) <= \elim p$-2 = $-3 (i.e. Id $-2 $-3)
  | trans-sym-l{A : universe 𝓤} -> {x : A} -> {y : A} -> (p : x = y) -> ((sym p) ⋅ p) = refl (i.e. {A : universe 𝓤} -> {x : A} -> {y : A} -> (p : Id x y) -> Id (trans (sym p) p) refl) refl{A : universe 𝓤} -> {x : A} -> x = x (i.e. {A : universe 𝓤} -> {x : A} -> Id x x) => refl{A : universe 𝓤} -> {x : A} -> x = x (i.e. {A : universe 𝓤} -> {x : A} -> Id x x)

\let trans-sym-r{A : universe 𝓤} -> {x : A} -> {y : A} -> (p : x = y) -> (p ⋅ (sym p)) = refl (i.e. {A : universe 𝓤} -> {x : A} -> {y : A} -> (p : Id x y) -> Id (trans p (sym p)) refl) {Auniverse 𝓤 : 𝓤universe S 𝓤} {xA yA : Auniverse 𝓤} : (px = y (i.e. Id x y) : xA = yA) -> (px = i (i.e. Id x i) ⋅ (sym{A : universe 𝓤} -> {x : A} -> {y : A} -> (_ : x = y) -> y = x (i.e. {A : universe 𝓤} -> {x : A} -> {y : A} -> (_ : Id x y) -> Id y x) px = i (i.e. Id x i))) = refl \where
  trans-sym-r px = y (i.e. Id x y) <= \elim p$-2 = $-3 (i.e. Id $-2 $-3)
  | trans-sym-r{A : universe 𝓤} -> {x : A} -> {y : A} -> (p : x = y) -> (p ⋅ (sym p)) = refl (i.e. {A : universe 𝓤} -> {x : A} -> {y : A} -> (p : Id x y) -> Id (trans p (sym p)) refl) refl{A : universe 𝓤} -> {x : A} -> x = x (i.e. {A : universe 𝓤} -> {x : A} -> Id x x) => refl{A : universe 𝓤} -> {x : A} -> x = x (i.e. {A : universe 𝓤} -> {x : A} -> Id x x)

Involution [local-2]

\let sym-sym{A : universe 𝓤} -> {x : A} -> {y : A} -> (p : x = y) -> (sym (sym p)) = p (i.e. {A : universe 𝓤} -> {x : A} -> {y : A} -> (p : Id x y) -> Id (sym (sym p)) p) {Auniverse 𝓤 : 𝓤universe S 𝓤} {xA yA : Auniverse 𝓤} : (px = y (i.e. Id x y) : xA = yA) -> (sym{A : universe 𝓤} -> {x : A} -> {y : A} -> (_ : x = y) -> y = x (i.e. {A : universe 𝓤} -> {x : A} -> {y : A} -> (_ : Id x y) -> Id y x) (sym{A : universe 𝓤} -> {x : A} -> {y : A} -> (_ : x = y) -> y = x (i.e. {A : universe 𝓤} -> {x : A} -> {y : A} -> (_ : Id x y) -> Id y x) px = i (i.e. Id x i))) = px = i (i.e. Id x i) \where
  sym-sym px = y (i.e. Id x y) <= \elim p$-2 = $-3 (i.e. Id $-2 $-3)
  | sym-sym{A : universe 𝓤} -> {x : A} -> {y : A} -> (p : x = y) -> (sym (sym p)) = p (i.e. {A : universe 𝓤} -> {x : A} -> {y : A} -> (p : Id x y) -> Id (sym (sym p)) p) refl{A : universe 𝓤} -> {x : A} -> x = x (i.e. {A : universe 𝓤} -> {x : A} -> Id x x) => refl{A : universe 𝓤} -> {x : A} -> x = x (i.e. {A : universe 𝓤} -> {x : A} -> Id x x)

Associativity [local-3]

\let trans-assoc{A : universe 𝓤} -> {w : A} -> {x : A} -> {y : A} -> {z : A} -> (p : w = x) -> (q : x = y) -> (r : y = z) -> ((p ⋅ q) ⋅ r) = (p ⋅ (q ⋅ r)) (i.e. {A : universe 𝓤} -> {w : A} -> {x : A} -> {y : A} -> {z : A} -> (p : Id w x) -> (q : Id x y) -> (r : Id y z) -> Id (trans (trans p q) r) (trans p (trans q r))) {Auniverse 𝓤 : 𝓤universe S 𝓤} {wA xA yA zA : Auniverse 𝓤}
  : (pw = x (i.e. Id w x) : wA = xA) -> (qi = y (i.e. Id i y) : xA = yA) -> (ry = z (i.e. Id y z) : yA = zA)
    -> (pw = i (i.e. Id w i) ⋅ qi = y (i.e. Id i y) ⋅ ry = z (i.e. Id y z)) = (pw = i (i.e. Id w i) ⋅ (qi = y (i.e. Id i y) ⋅ ry = z (i.e. Id y z))) \where
  trans-assoc pw = x (i.e. Id w x) qx = y (i.e. Id x y) ry = z (i.e. Id y z) <= \elim p$-2 = $-3 (i.e. Id $-2 $-3)
  | trans-assoc{A : universe 𝓤} -> {w : A} -> {x : A} -> {y : A} -> {z : A} -> (p : w = x) -> (q : x = y) -> (r : y = z) -> ((p ⋅ q) ⋅ r) = (p ⋅ (q ⋅ r)) (i.e. {A : universe 𝓤} -> {w : A} -> {x : A} -> {y : A} -> {z : A} -> (p : Id w x) -> (q : Id x y) -> (r : Id y z) -> Id (trans (trans p q) r) (trans p (trans q r))) refl{A : universe 𝓤} -> {x : A} -> x = x (i.e. {A : universe 𝓤} -> {x : A} -> Id x x) q r => refl{A : universe 𝓤} -> {x : A} -> x = x (i.e. {A : universe 𝓤} -> {x : A} -> Id x x)