feat(homotopy/torus): give recursion and induction principle for the torus

also change the surface of the torus to a square instead of an equality between paths

hott/cubical/square.hlean

@@ -88,7 +88,7 @@ namespace eq
   definition transpose [unfold 10] (s₁₁ : square p₁₀ p₁₂ p₀₁ p₂₁) : square p₀₁ p₂₁ p₁₀ p₁₂ :=
   by induction s₁₁;exact ids
 
-  definition aps {B : Type} (f : A → B) (s₁₁ : square p₁₀ p₁₂ p₀₁ p₂₁)
+  definition aps [unfold 12] {B : Type} (f : A → B) (s₁₁ : square p₁₀ p₁₂ p₀₁ p₂₁)
     : square (ap f p₁₀) (ap f p₁₂) (ap f p₀₁) (ap f p₂₁) :=
   by induction s₁₁;exact ids
 

hott/cubical/square2.hlean

@@ -8,10 +8,12 @@ Coherence conditions for operations on squares
 
 import .square
 
+open equiv
+
 namespace eq
 
   variables {A B C : Type} {a a' a'' a₀₀ a₂₀ a₄₀ a₀₂ a₂₂ a₂₄ a₀₄ a₄₂ a₄₄ a₁ a₂ a₃ a₄ : A}
-            {b : B} {c : C}
+            {f : A → B} {b : B} {c : C}
             /-a₀₀-/ {p₁₀ p₁₀' : a₀₀ = a₂₀} /-a₂₀-/ {p₃₀ : a₂₀ = a₄₀} /-a₄₀-/
        {p₀₁ p₀₁' : a₀₀ = a₀₂} /-s₁₁-/ {p₂₁ p₂₁' : a₂₀ = a₂₂} /-s₃₁-/ {p₄₁ : a₄₀ = a₄₂}
             /-a₀₂-/ {p₁₂ p₁₂' : a₀₂ = a₂₂} /-a₂₂-/ {p₃₂ : a₂₂ = a₄₂} /-a₄₂-/
@@ -31,4 +33,20 @@ namespace eq
     {s₁₁' : square p₁₀ p₁₂ p p₂₁} (t : s₁₁ = r ⬝ph s₁₁') : r⁻¹ ⬝ph s₁₁ = s₁₁' :=
   by induction r; exact t
 
+  -- the following is used for torus.elim_surf
+  theorem whisker_square_aps_eq
+    {q₁₀ : f a₀₀ = f a₂₀} {q₀₁ : f a₀₀ = f a₀₂} {q₂₁ : f a₂₀ = f a₂₂} {q₁₂ : f a₀₂ = f a₂₂}
+    {r₁₀ : ap f p₁₀ = q₁₀} {r₀₁ : ap f p₀₁ = q₀₁} {r₂₁ : ap f p₂₁ = q₂₁} {r₁₂ : ap f p₁₂ = q₁₂}
+    {s₁₁ : p₁₀ ⬝ p₂₁ = p₀₁ ⬝ p₁₂} {t₁₁ : square q₁₀ q₁₂ q₀₁ q₂₁}
+    (u : square (ap02 f s₁₁) (eq_of_square t₁₁)
+                (ap_con f p₁₀ p₂₁ ⬝ (r₁₀ ◾ r₂₁)) (ap_con f p₀₁ p₁₂ ⬝ (r₀₁ ◾ r₁₂)))
+    : whisker_square r₁₀ r₁₂ r₀₁ r₂₁ (aps f (square_of_eq s₁₁)) = t₁₁ :=
+  begin
+    induction r₁₀, induction r₀₁, induction r₁₂, induction r₂₁,
+    induction p₁₂, induction p₁₀, induction p₂₁, esimp at *, induction s₁₁, esimp at *,
+    esimp [square_of_eq],
+    apply eq_of_fn_eq_fn !square_equiv_eq, esimp,
+    exact (eq_bot_of_square u)⁻¹
+  end
+
 end eq

hott/hit/set_quotient.hlean

@@ -13,8 +13,8 @@ open eq is_trunc trunc quotient equiv
 namespace set_quotient
 section
   parameters {A : Type} (R : A → A → hprop)
-  -- set-quotients are just truncations of (type) quotients
-  definition set_quotient : Type := trunc 0 (quotient (λa a', trunctype.carrier (R a a')))
+  -- set-quotients are just set-truncations of (type) quotients
+  definition set_quotient : Type := trunc 0 (quotient R)
 
   parameter {R}
   definition class_of (a : A) : set_quotient :=
@@ -71,11 +71,6 @@ section
     : P :=
   elim Pc (λa a' H, !is_hprop.elim) x
 
-  /-
-    there are no theorems to eliminate to the universe here,
-    because the universe is generally not a set
-  -/
-
 end
 end set_quotient
 

hott/hit/trunc.hlean

@@ -24,11 +24,6 @@ namespace trunc
     [Pt : is_trunc n P] (H : A → P) : P :=
   trunc.elim H aa
 
-  /-
-    there are no theorems to eliminate to the universe here,
-    because the universe is not a set
-  -/
-
 end trunc
 
 attribute trunc.elim_on [unfold 4]

hott/hit/two_quotient.hlean

@@ -345,7 +345,7 @@ namespace two_quotient
              (R : A → A → Type)
   local abbreviation T := e_closure R -- the (type-valued) equivalence closure of R
   parameter  (Q : Π⦃a a'⦄, T a a' → T a a' → Type)
-  variables ⦃a a' : A⦄ {s : R a a'} {t t' : T a a'}
+  variables ⦃a a' a'' : A⦄ {s : R a a'} {t t' : T a a'}
 
   inductive two_quotient_Q : Π⦃a : A⦄, e_closure R a a → Type :=
   | Qmk : Π⦃a a' : A⦄ ⦃t t' : T a a'⦄, Q t t' → two_quotient_Q (t ⬝r t'⁻¹ʳ)
@@ -369,14 +369,14 @@ namespace two_quotient
     induction x,
     { exact P0 a},
     { exact P1 s},
-    { induction q with a a' t t' q,
+    { exact abstract [irreducible] begin induction q with a a' t t' q,
       rewrite [elimo_con (simple_two_quotient.incl1 R Q2) P1,
                elimo_inv (simple_two_quotient.incl1 R Q2) P1,
                -whisker_right_eq_of_con_inv_eq_idp (simple_two_quotient.incl2 R Q2 (Qmk R q)),
                change_path_con],
       xrewrite [change_path_cono],
       refine ap (λx, change_path _ (_ ⬝o x)) !change_path_invo ⬝ _, esimp,
-      apply cono_invo_eq_idpo, apply P2}
+      apply cono_invo_eq_idpo, apply P2 end end}
   end
 
   protected definition rec_on [reducible] {P : two_quotient → Type} (x : two_quotient)
@@ -455,6 +455,31 @@ namespace two_quotient
     apply top_deg_square
   end
 
+  definition elim_inclt_rel [unfold_full] {P : Type} {P0 : A → P}
+    {P1 : Π⦃a a' : A⦄ (s : R a a'), P0 a = P0 a'}
+    (P2 : Π⦃a a' : A⦄ ⦃t t' : T a a'⦄ (q : Q t t'), e_closure.elim P1 t = e_closure.elim P1 t')
+    ⦃a a' : A⦄ (r : R a a') : elim_inclt P2 [r] = elim_incl1 P2 r :=
+  idp
+
+  definition elim_inclt_inv [unfold_full] {P : Type} {P0 : A → P}
+    {P1 : Π⦃a a' : A⦄ (s : R a a'), P0 a = P0 a'}
+    (P2 : Π⦃a a' : A⦄ ⦃t t' : T a a'⦄ (q : Q t t'), e_closure.elim P1 t = e_closure.elim P1 t')
+    ⦃a a' : A⦄ (t : T a a')
+    : elim_inclt P2 t⁻¹ʳ = ap_inv (elim P0 P1 P2) (inclt t) ⬝ (elim_inclt P2 t)⁻² :=
+  idp
+
+  definition elim_inclt_con [unfold_full] {P : Type} {P0 : A → P}
+    {P1 : Π⦃a a' : A⦄ (s : R a a'), P0 a = P0 a'}
+    (P2 : Π⦃a a' : A⦄ ⦃t t' : T a a'⦄ (q : Q t t'), e_closure.elim P1 t = e_closure.elim P1 t')
+    ⦃a a' a'' : A⦄ (t : T a a') (t': T a' a'')
+    : elim_inclt P2 (t ⬝r t') =
+        ap_con (elim P0 P1 P2) (inclt t) (inclt t') ⬝ (elim_inclt P2 t ◾ elim_inclt P2 t') :=
+  idp
+
+  definition inclt_rel [unfold_full] (r : R a a') : inclt [r] = incl1 r := idp
+  definition inclt_inv [unfold_full] (t : T a a') : inclt t⁻¹ʳ = (inclt t)⁻¹ := idp
+  definition inclt_con [unfold_full] (t : T a a') (t' : T a' a'')
+    : inclt (t ⬝r t') = inclt t ⬝ inclt t' := idp
 end
 end two_quotient
 

hott/homotopy/torus.hlean

@@ -9,10 +9,11 @@ Declaration of the torus
 
 import hit.two_quotient
 
-open two_quotient eq bool unit relation
+open two_quotient eq bool unit equiv
 
 namespace torus
 
+  open e_closure relation
   definition torus_R (x y : unit) := bool
   local infix `⬝r`:75 := @e_closure.trans unit torus_R star star star
   local postfix `⁻¹ʳ`:(max+10) := @e_closure.symm unit torus_R star star
@@ -21,73 +22,79 @@ namespace torus
   inductive torus_Q : Π⦃x y : unit⦄, e_closure torus_R x y → e_closure torus_R x y → Type :=
   | Qmk : torus_Q ([ff] ⬝r [tt]) ([tt] ⬝r [ff])
 
+  open torus_Q
+
   definition torus := two_quotient torus_R torus_Q
+  notation `T²` := torus
   definition base  : torus := incl0 _ _ star
   definition loop1 : base = base := incl1 _ _ ff
   definition loop2 : base = base := incl1 _ _ tt
-  definition surf  : loop1 ⬝ loop2 = loop2 ⬝ loop1 :=
-  incl2 _ _ torus_Q.Qmk
+  definition surf' : loop1 ⬝ loop2 = loop2 ⬝ loop1 :=
+  incl2 _ _ Qmk
+  definition surf  : square loop1 loop1 loop2 loop2 :=
+  square_of_eq (incl2 _ _ Qmk)
 
-  -- protected definition rec {P : torus → Type} (Pb : P base) (Pl1 : Pb =[loop1] Pb)
-  --   (Pl2 : Pb =[loop2] Pb) (Pf : squareover P fill Pl1 Pl1 Pl2 Pl2)
-  --   (x : torus) : P x :=
-  -- sorry
+  protected definition rec {P : torus → Type} (Pb : P base) (Pl1 : Pb =[loop1] Pb)
+    (Pl2 : Pb =[loop2] Pb) (Ps : squareover P surf Pl1 Pl1 Pl2 Pl2) (x : torus) : P x :=
+  begin
+    induction x,
+    { induction a, exact Pb},
+    { induction s: induction a; induction a',
+      { exact Pl1},
+      { exact Pl2}},
+    { induction q, esimp, apply change_path_of_pathover, apply pathover_of_squareover, exact Ps},
+  end
 
-  -- example {P : torus → Type} (Pb : P base) (Pl1 : Pb =[loop1] Pb) (Pl2 : Pb =[loop2] Pb)
-  --         (Pf : squareover P fill Pl1 Pl1 Pl2 Pl2) : torus.rec Pb Pl1 Pl2 Pf base = Pb := idp
+  protected definition rec_on [reducible] {P : torus → Type} (x : torus) (Pb : P base)
+    (Pl1 : Pb =[loop1] Pb) (Pl2 : Pb =[loop2] Pb) (Ps : squareover P surf Pl1 Pl1 Pl2 Pl2) : P x :=
+  torus.rec Pb Pl1 Pl2 Ps x
 
-  -- definition rec_loop1 {P : torus → Type} (Pb : P base) (Pl1 : Pb =[loop1] Pb)
-  --   (Pl2 : Pb =[loop2] Pb) (Pf : squareover P fill Pl1 Pl1 Pl2 Pl2)
-  --   : apdo (torus.rec Pb Pl1 Pl2 Pf) loop1 = Pl1 :=
-  -- sorry
+  theorem rec_loop1 {P : torus → Type} (Pb : P base) (Pl1 : Pb =[loop1] Pb)
+    (Pl2 : Pb =[loop2] Pb) (Ps : squareover P surf Pl1 Pl1 Pl2 Pl2)
+    : apdo (torus.rec Pb Pl1 Pl2 Ps) loop1 = Pl1 :=
+  !rec_incl1
 
-  -- definition rec_loop2 {P : torus → Type} (Pb : P base) (Pl1 : Pb =[loop1] Pb)
-  --   (Pl2 : Pb =[loop2] Pb) (Pf : squareover P fill Pl1 Pl1 Pl2 Pl2)
-  --   : apdo (torus.rec Pb Pl1 Pl2 Pf) loop2 = Pl2 :=
-  -- sorry
-
-  -- definition rec_surf {P : torus → Type} (Pb : P base) (Pl1 : Pb =[loop1] Pb)
-  --   (Pl2 : Pb =[loop2] Pb) (Pf : squareover P fill Pl1 Pl1 Pl2 Pl2)
-  --   : cubeover P rfl1 (apds (torus.rec Pb Pl1 Pl2 Pf) fill) Pf
-  --              (vdeg_squareover !rec_loop2) (vdeg_squareover !rec_loop2)
-  --              (vdeg_squareover !rec_loop1) (vdeg_squareover !rec_loop1) :=
-  -- sorry
+  theorem rec_loop2 {P : torus → Type} (Pb : P base) (Pl1 : Pb =[loop1] Pb)
+    (Pl2 : Pb =[loop2] Pb) (Ps : squareover P surf Pl1 Pl1 Pl2 Pl2)
+    : apdo (torus.rec Pb Pl1 Pl2 Ps) loop2 = Pl2 :=
+  !rec_incl1
 
   protected definition elim {P : Type} (Pb : P) (Pl1 : Pb = Pb) (Pl2 : Pb = Pb)
-    (Ps : Pl1 ⬝ Pl2 = Pl2 ⬝ Pl1) (x : torus) : P :=
+    (Ps : square Pl1 Pl1 Pl2 Pl2) (x : torus) : P :=
   begin
     induction x,
     { exact Pb},
     { induction s,
       { exact Pl1},
       { exact Pl2}},
-    { induction q, exact Ps},
+    { induction q, apply eq_of_square, exact Ps},
   end
 
   protected definition elim_on [reducible] {P : Type} (x : torus) (Pb : P)
-    (Pl1 : Pb = Pb) (Pl2 : Pb = Pb) (Ps : Pl1 ⬝ Pl2 = Pl2 ⬝ Pl1) : P :=
+    (Pl1 : Pb = Pb) (Pl2 : Pb = Pb) (Ps : square Pl1 Pl1 Pl2 Pl2) : P :=
   torus.elim Pb Pl1 Pl2 Ps x
 
-  definition elim_loop1 {P : Type} (Pb : P) (Pl1 : Pb = Pb) (Pl2 : Pb = Pb)
-    (Ps : Pl1 ⬝ Pl2 = Pl2 ⬝ Pl1) : ap (torus.elim Pb Pl1 Pl2 Ps) loop1 = Pl1 :=
+  definition elim_loop1 {P : Type} {Pb : P} {Pl1 : Pb = Pb} {Pl2 : Pb = Pb}
+    (Ps : square Pl1 Pl1 Pl2 Pl2) : ap (torus.elim Pb Pl1 Pl2 Ps) loop1 = Pl1 :=
   !elim_incl1
 
-  definition elim_loop2 {P : Type} (Pb : P) (Pl1 : Pb = Pb) (Pl2 : Pb = Pb)
-    (Ps : Pl1 ⬝ Pl2 = Pl2 ⬝ Pl1) : ap (torus.elim Pb Pl1 Pl2 Ps) loop2 = Pl2 :=
+  definition elim_loop2 {P : Type} {Pb : P} {Pl1 : Pb = Pb} {Pl2 : Pb = Pb}
+    (Ps : square Pl1 Pl1 Pl2 Pl2) : ap (torus.elim Pb Pl1 Pl2 Ps) loop2 = Pl2 :=
   !elim_incl1
 
-  theorem elim_surf {P : Type} (Pb : P) (Pl1 : Pb = Pb) (Pl2 : Pb = Pb)
-    (Ps : Pl1 ⬝ Pl2 = Pl2 ⬝ Pl1)
-    : square (ap02 (torus.elim Pb Pl1 Pl2 Ps) surf)
-             Ps
-             (!ap_con ⬝ (!elim_loop1 ◾ !elim_loop2))
-             (!ap_con ⬝ (!elim_loop2 ◾ !elim_loop1)) :=
-  !elim_incl2
+  theorem elim_surf {P : Type} {Pb : P} {Pl1 : Pb = Pb} {Pl2 : Pb = Pb}
+    (Ps : square Pl1 Pl1 Pl2 Pl2)
+    : whisker_square (elim_loop1 Ps) (elim_loop1 Ps) (elim_loop2 Ps) (elim_loop2 Ps)
+                     (aps (torus.elim Pb Pl1 Pl2 Ps) surf) = Ps :=
+  begin
+    apply whisker_square_aps_eq,
+    apply elim_incl2
+  end
 
 end torus
 
 attribute torus.base [constructor]
-attribute /-torus.rec-/ torus.elim [unfold 6] [recursor 6]
---attribute torus.elim_type [unfold 9]
-attribute /-torus.rec_on-/ torus.elim_on [unfold 2]
---attribute torus.elim_type_on [unfold 6]
+attribute torus.rec torus.elim [unfold 6] [recursor 6]
+--attribute torus.elim_type [unfold 5]
+attribute torus.rec_on torus.elim_on [unfold 2]
+--attribute torus.elim_type_on [unfold 1]

hott/init/path.hlean

@@ -265,12 +265,12 @@ namespace eq
   -- functorial.
 
   -- Functions take identity paths to identity paths
-  definition ap_idp (x : A) (f : A → B) : ap f idp = idp :> (f x = f x) := idp
+  definition ap_idp [unfold_full] (x : A) (f : A → B) : ap f idp = idp :> (f x = f x) := idp
 
   -- Functions commute with concatenation.
-  definition ap_con (f : A → B) {x y z : A} (p : x = y) (q : y = z) :
+  definition ap_con [unfold 8] (f : A → B) {x y z : A} (p : x = y) (q : y = z) :
     ap f (p ⬝ q) = ap f p ⬝ ap f q :=
-  eq.rec_on q (eq.rec_on p idp)
+  eq.rec_on q idp
 
   definition con_ap_con_eq_con_ap_con_ap (f : A → B) {w x y z : A} (r : f w = f x)
     (p : x = y) (q : y = z) : r ⬝ ap f (p ⬝ q) = (r ⬝ ap f p) ⬝ ap f q :=
@@ -281,15 +281,15 @@ namespace eq
   eq.rec_on q (eq.rec_on p (take r, con.assoc _ _ _)) r
 
   -- Functions commute with path inverses.
-  definition ap_inv' (f : A → B) {x y : A} (p : x = y) : (ap f p)⁻¹ = ap f p⁻¹ :=
+  definition ap_inv' [unfold 6] (f : A → B) {x y : A} (p : x = y) : (ap f p)⁻¹ = ap f p⁻¹ :=
   eq.rec_on p idp
 
-  definition ap_inv {A B : Type} (f : A → B) {x y : A} (p : x = y) : ap f p⁻¹ = (ap f p)⁻¹ :=
+  definition ap_inv [unfold 6] (f : A → B) {x y : A} (p : x = y) : ap f p⁻¹ = (ap f p)⁻¹ :=
   eq.rec_on p idp
 
   -- [ap] itself is functorial in the first argument.
 
-  definition ap_id (p : x = y) : ap id p = p :=
+  definition ap_id [unfold 4] (p : x = y) : ap id p = p :=
   eq.rec_on p idp
 
   definition ap_compose [unfold 8] (g : B → C) (f : A → B) {x y : A} (p : x = y) :

src/emacs/lean-syntax.el

@@ -37,7 +37,7 @@
     "→" "∃" "∀" "∘" "×" "Σ" "Π" "~" "||" "&&" "≃" "≡" "≅"
     "ℕ" "ℤ" "ℚ" "ℝ" "ℂ" "𝔸"
     ;; HoTT notation
-    "Ω" "∥" "map₊" "₊" "π₁" "S¹" "⇒" "⟹" "⟶"
+    "Ω" "∥" "map₊" "₊" "π₁" "S¹" "T²" "⇒" "⟹" "⟶"
     "⁻¹ᵉ" "⁻¹ᶠ" "⁻¹ᵍ" "⁻¹ʰ" "⁻¹ⁱ" "⁻¹ᵐ" "⁻¹ᵒ" "⁻¹ᵖ" "⁻¹ʳ" "⁻¹ᵛ" "⁻¹ˢ" "⁻²" "⁻²ᵒ"
     "⬝e" "⬝i" "⬝o" "⬝op" "⬝po" "⬝h" "⬝v" "⬝hp" "⬝vp" "⬝ph" "⬝pv" "⬝r" "◾" "◾o"
     "∘n" "∘f" "∘fi" "∘nf" "∘fn" "∘n1f" "∘1nf" "∘f1n" "∘fn1"