feat(types): incorporate pathovers in the files of the types folder

Conflicts:
	hott/cubical/pathover.hlean

hott/algebra/category/nat_trans.hlean

@@ -70,9 +70,8 @@ namespace nat_trans
     intro η, apply nat_trans_eq, intro a, apply idp,
     intro S,
     fapply sigma_eq,
-      apply eq_of_homotopy, intro a,
+    { apply eq_of_homotopy, intro a, apply idp},
-      apply idp,
+    { apply is_hprop.elimo}
-    apply is_hprop.elim,
   end
 
   definition is_hset_nat_trans [instance] : is_hset (F ⟹ G) :=

hott/algebra/hott.hlean

@@ -41,7 +41,7 @@ namespace algebra
     cases ps, cases ph1, cases ph2, cases ph3, cases ph4, reflexivity
   end
 
-  definition group_pathover {G : group A} {H : group B} (f : A ≃ B) : (Π(g h : A), f (g * h) = f g * f h) → G =[ua f] H :=
+  definition group_pathover {G : group A} {H : group B} {f : A ≃ B} : (Π(g h : A), f (g * h) = f g * f h) → G =[ua f] H :=
   begin
     revert H,
     eapply (rec_on_ua_idp' f),

hott/core.hlean

@@ -7,6 +7,5 @@ The core of the HoTT library
 -/
 
 import types
-import cubical.square
 import hit.circle
 import algebra.hott

hott/init/equiv.hlean

@@ -261,6 +261,11 @@ namespace equiv
   protected definition trans [trans] (f : A ≃ B) (g: B ≃ C) : A ≃ C :=
   equiv.mk (g ∘ f) !is_equiv_compose
 
+  infixl `⬝e`:75 := equiv.trans
+  postfix [parsing-only] `⁻¹ᵉ`:(max + 1) := equiv.symm
+    -- notation for inverse which is not overloaded
+  abbreviation erfl [constructor] := @equiv.refl
+
   definition equiv_of_eq_fn_of_equiv (f : A ≃ B) {f' : A → B} (Heq : f = f') : A ≃ B :=
   equiv.mk f' (is_equiv_eq_closed Heq)
 
@@ -287,11 +292,7 @@ namespace equiv
   definition equiv_of_eq_of_equiv {A B C : Type} (p : A ≃ B) (q : B = C) : A ≃ C := q   ▸ p
 
   namespace ops
-    infixl `⬝e`:75 := equiv.trans
     postfix `⁻¹` := equiv.symm -- overloaded notation for inverse
-    postfix [parsing-only] `⁻¹ᵉ`:(max + 1) := equiv.symm
-      -- notation for inverse which is not overloaded
-    abbreviation erfl [constructor] := @equiv.refl
   end ops
 end equiv
 

hott/types/W.hlean

@@ -7,7 +7,7 @@ Theorems about W-types (well-founded trees)
 -/
 
 import .sigma .pi
-open eq sigma sigma.ops equiv is_equiv
+open eq equiv is_equiv sigma sigma.ops
 
 inductive Wtype.{l k} {A : Type.{l}} (B : A → Type.{k}) : Type.{max l k} :=
 sup : Π (a : A), (B a → Wtype.{l k} B) → Wtype.{l k} B
@@ -35,71 +35,71 @@ namespace Wtype
   protected definition eta (w : W a, B a) : ⟨w.1 , w.2⟩ = w :=
   by cases w; exact idp
 
-  definition sup_eq_sup (p : a = a') (q : p ▸ f = f') : ⟨a, f⟩ = ⟨a', f'⟩ :=
+  definition sup_eq_sup (p : a = a') (q : f =[p] f') : ⟨a, f⟩ = ⟨a', f'⟩ :=
-  by cases p; cases q; exact idp
+  by cases q; exact idp
 
-  definition Wtype_eq (p : w.1 = w'.1) (q : p ▸ w.2 = w'.2) : w = w' :=
+  definition Wtype_eq (p : w.1 = w'.1) (q : w.2 =[p] w'.2) : w = w' :=
   by cases w; cases w';exact (sup_eq_sup p q)
 
   definition Wtype_eq_pr1 (p : w = w') : w.1 = w'.1 :=
   by cases p;exact idp
 
-  definition Wtype_eq_pr2 (p : w = w') : Wtype_eq_pr1 p ▸ w.2 = w'.2 :=
+  definition Wtype_eq_pr2 (p : w = w') : w.2 =[Wtype_eq_pr1 p] w'.2 :=
-  by cases p;exact idp
+  by cases p;exact idpo
 
   namespace ops
   postfix `..1`:(max+1) := Wtype_eq_pr1
   postfix `..2`:(max+1) := Wtype_eq_pr2
   end ops open ops open sigma
 
-  definition sup_path_W (p : w.1 = w'.1) (q : p ▸ w.2 = w'.2)
+  definition sup_path_W (p : w.1 = w'.1) (q : w.2 =[p] w'.2)
-      :  ⟨(Wtype_eq p q)..1,(Wtype_eq p q)..2⟩ = ⟨p, q⟩ :=
+    : ⟨(Wtype_eq p q)..1, (Wtype_eq p q)..2⟩ = ⟨p, q⟩ :=
-  by cases w; cases w'; cases p; cases q; exact idp
+  by cases w; cases w'; cases q; exact idp
 
-  definition pr1_path_W (p : w.1 = w'.1) (q : p ▸ w.2 = w'.2) : (Wtype_eq p q)..1 = p :=
+  definition pr1_path_W (p : w.1 = w'.1) (q : w.2 =[p] w'.2) : (Wtype_eq p q)..1 = p :=
   !sup_path_W..1
 
-  definition pr2_path_W (p : w.1 = w'.1) (q : p ▸ w.2 = w'.2)
+  definition pr2_path_W (p : w.1 = w'.1) (q : w.2 =[p] w'.2)
-      : pr1_path_W p q ▸ (Wtype_eq p q)..2 = q :=
+      : (Wtype_eq p q)..2 =[pr1_path_W p q] q :=
   !sup_path_W..2
 
   definition eta_path_W (p : w = w') : Wtype_eq (p..1) (p..2) = p :=
   by cases p; cases w; exact idp
 
-  definition transport_pr1_path_W {B' : A → Type} (p : w.1 = w'.1) (q : p ▸ w.2 = w'.2)
+  definition transport_pr1_path_W {B' : A → Type} (p : w.1 = w'.1) (q : w.2 =[p] w'.2)
       : transport (λx, B' x.1) (Wtype_eq p q) = transport B' p :=
-  by cases w; cases w'; cases p; cases q; exact idp
+  by cases w; cases w'; cases q; exact idp
 
-  definition path_W_uncurried (pq : Σ(p : w.1 = w'.1), p ▸ w.2 = w'.2) : w = w' :=
+  definition path_W_uncurried (pq : Σ(p : w.1 = w'.1), w.2 =[p] w'.2) : w = w' :=
   by cases pq with p q; exact (Wtype_eq p q)
 
-  definition sup_path_W_uncurried (pq : Σ(p : w.1 = w'.1), p ▸ w.2 = w'.2)
+  definition sup_path_W_uncurried (pq : Σ(p : w.1 = w'.1), w.2 =[p] w'.2)
       :  ⟨(path_W_uncurried pq)..1, (path_W_uncurried pq)..2⟩ = pq :=
   by cases pq with p q; exact (sup_path_W p q)
 
-  definition pr1_path_W_uncurried (pq : Σ(p : w.1 = w'.1), p ▸ w.2 = w'.2)
+  definition pr1_path_W_uncurried (pq : Σ(p : w.1 = w'.1), w.2 =[p] w'.2)
       : (path_W_uncurried pq)..1 = pq.1 :=
   !sup_path_W_uncurried..1
 
-  definition pr2_path_W_uncurried (pq : Σ(p : w.1 = w'.1), p ▸ w.2 = w'.2)
+  definition pr2_path_W_uncurried (pq : Σ(p : w.1 = w'.1), w.2 =[p] w'.2)
-      : (pr1_path_W_uncurried pq) ▸ (path_W_uncurried pq)..2 = pq.2 :=
+      : (path_W_uncurried pq)..2 =[pr1_path_W_uncurried pq] pq.2 :=
   !sup_path_W_uncurried..2
 
   definition eta_path_W_uncurried (p : w = w') : path_W_uncurried ⟨p..1, p..2⟩ = p :=
   !eta_path_W
 
-  definition transport_pr1_path_W_uncurried {B' : A → Type} (pq : Σ(p : w.1 = w'.1), p ▸ w.2 = w'.2)
+  definition transport_pr1_path_W_uncurried {B' : A → Type} (pq : Σ(p : w.1 = w'.1), w.2 =[p] w'.2)
       : transport (λx, B' x.1) (@path_W_uncurried A B w w' pq) = transport B' pq.1 :=
   by cases pq with p q; exact (transport_pr1_path_W p q)
 
   definition isequiv_path_W /-[instance]-/ (w w' : W a, B a)
-      : is_equiv (@path_W_uncurried A B w w') :=
+      : is_equiv (path_W_uncurried : (Σ(p : w.1 = w'.1), w.2 =[p] w'.2) → w = w') :=
   adjointify path_W_uncurried
              (λp, ⟨p..1, p..2⟩)
              eta_path_W_uncurried
              sup_path_W_uncurried
 
-  definition equiv_path_W (w w' : W a, B a) : (Σ(p : w.1 = w'.1),  p ▸ w.2 = w'.2) ≃ (w = w') :=
+  definition equiv_path_W (w w' : W a, B a) : (Σ(p : w.1 = w'.1), w.2 =[p] w'.2) ≃ (w = w') :=
   equiv.mk path_W_uncurried !isequiv_path_W
 
   definition double_induction_on {P : (W a, B a) → (W a, B a) → Type} (w w' : W a, B a)
@@ -115,7 +115,7 @@ namespace Wtype
   end
 
   /- truncatedness -/
-  open is_trunc
+  open is_trunc pi
   definition trunc_W [instance] (n : trunc_index)
     [HA : is_trunc (n.+1) A] : is_trunc (n.+1) (W a, B a) :=
   begin
@@ -123,9 +123,9 @@ namespace Wtype
   eapply (double_induction_on w w'), intro a a' f f' IH,
   fapply is_trunc_equiv_closed,
   { apply equiv_path_W},
-  { fapply is_trunc_sigma,
+  { apply is_trunc_sigma,
-    intro p, cases p, esimp,
+    intro p, cases p, esimp, apply is_trunc_equiv_closed_rev,
-    apply pi.is_trunc_eq_pi}
+      apply pathover_idp}
   end
 
 end Wtype

hott/types/default.hlean

@@ -4,5 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Floris van Doorn
 -/
 
-import .sigma .prod .pi .equiv .fiber .eq .trunc .arrow .pointed .function .trunc .bool
+import .sigma .prod .pi .equiv .fiber .trunc .arrow .pointed .function .trunc .bool
+import .eq .square
 import .nat .int

hott/types/eq.hlean

@@ -3,11 +3,11 @@ Copyright (c) 2014 Floris van Doorn. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Author: Floris van Doorn
 
-Ported from Coq HoTT
+Partially ported from Coq HoTT
 Theorems about path types (identity types)
 -/
 
-open eq sigma sigma.ops equiv is_equiv
+open eq sigma sigma.ops equiv is_equiv equiv.ops
 
 namespace eq
   /- Path spaces -/
@@ -22,31 +22,31 @@ namespace eq
   definition whisker_left_con_right (p : a1 = a2) {q q' q'' : a2 = a3} (r : q = q') (s : q' = q'')
     : whisker_left p (r ⬝ s) = whisker_left p r ⬝ whisker_left p s :=
   begin
-    cases p, cases r, cases s, apply idp
+    cases p, cases r, cases s, exact idp
   end
 
   definition whisker_right_con_right {p p' p'' : a1 = a2} (q : a2 = a3) (r : p = p') (s : p' = p'')
     : whisker_right (r ⬝ s) q = whisker_right r q ⬝ whisker_right s q :=
   begin
-    cases q, cases r, cases s, apply idp
+    cases q, cases r, cases s, exact idp
   end
 
   definition whisker_left_con_left (p : a1 = a2) (p' : a2 = a3) {q q' : a3 = a4} (r : q = q')
     : whisker_left (p ⬝ p') r = !con.assoc ⬝ whisker_left p (whisker_left p' r) ⬝ !con.assoc' :=
   begin
-    cases p', cases p, cases r, cases q, apply idp
+    cases p', cases p, cases r, cases q, exact idp
   end
 
   definition whisker_right_con_left {p p' : a1 = a2} (q : a2 = a3) (q' : a3 = a4) (r : p = p')
     : whisker_right r (q ⬝ q') = !con.assoc' ⬝ whisker_right (whisker_right r q) q' ⬝ !con.assoc :=
   begin
-    cases q', cases q, cases r, cases p, apply idp
+    cases q', cases q, cases r, cases p, exact idp
   end
 
   definition whisker_left_inv_left (p : a2 = a1) {q q' : a2 = a3} (r : q = q')
     : !con_inv_cancel_left⁻¹ ⬝ whisker_left p (whisker_left p⁻¹ r) ⬝ !con_inv_cancel_left = r :=
   begin
-    cases p, cases r, cases q, apply idp
+    cases p, cases r, cases q, exact idp
   end
 
   /- Transporting in path spaces.
@@ -68,61 +68,66 @@ namespace eq
 
   definition transport_eq_lr (p : a1 = a2) (q : a1 = a1)
     : transport (λx, x = x) p q = p⁻¹ ⬝ q ⬝ p :=
-  begin
+  by cases p; rewrite [▸*,idp_con]
-  cases p,
-  symmetry, transitivity (refl a1)⁻¹ ⬝ q,
-    apply con_idp,
-    apply idp_con
-  end
 
   definition transport_eq_Fl (p : a1 = a2) (q : f a1 = b)
     : transport (λx, f x = b) p q = (ap f p)⁻¹ ⬝ q :=
-  by cases p; cases q; apply idp
+  by cases p; cases q; reflexivity
 
   definition transport_eq_Fr (p : a1 = a2) (q : b = f a1)
     : transport (λx, b = f x) p q = q ⬝ (ap f p) :=
-  by cases p; apply idp
+  by cases p; reflexivity
 
   definition transport_eq_FlFr (p : a1 = a2) (q : f a1 = g a1)
     : transport (λx, f x = g x) p q = (ap f p)⁻¹ ⬝ q ⬝ (ap g p) :=
-  begin
+  by cases p; rewrite [▸*,idp_con]
-  cases p,
-  symmetry, transitivity (ap f (refl a1))⁻¹ ⬝ q,
-    apply con_idp,
-    apply idp_con
-  end
 
   definition transport_eq_FlFr_D {B : A → Type} {f g : Πa, B a}
     (p : a1 = a2) (q : f a1 = g a1)
       : transport (λx, f x = g x) p q = (apd f p)⁻¹ ⬝ ap (transport B p) q ⬝ (apd g p) :=
-  begin
+  by cases p; rewrite [▸*,idp_con,ap_id]
-  cases p,
-  symmetry,
-  transitivity _,
-    apply con_idp,
-    transitivity _,
-      apply idp_con,
-      apply ap_id
-  end
 
   definition transport_eq_FFlr (p : a1 = a2) (q : h (f a1) = a1)
     : transport (λx, h (f x) = x) p q = (ap h (ap f p))⁻¹ ⬝ q ⬝ p :=
-  begin
+  by cases p; rewrite [▸*,idp_con]
-  cases p,
-  symmetry,
-  transitivity (ap h (ap f (refl a1)))⁻¹ ⬝ q,
-     apply con_idp,
-     apply idp_con,
-  end
 
   definition transport_eq_lFFr (p : a1 = a2) (q : a1 = h (f a1))
     : transport (λx, x = h (f x)) p q = p⁻¹ ⬝ q ⬝ (ap h (ap f p)) :=
-  begin
+  by cases p; rewrite [▸*,idp_con]
-  cases p, symmetry,
+
-  transitivity (refl a1)⁻¹ ⬝ q,
+  /- Pathovers -/
-    apply con_idp,
+
-    apply idp_con,
+  -- In the comment we give the fibration of the pathover
-  end
+  definition pathover_eq_l (p : a1 = a2) (q : a1 = a3) : q =[p] p⁻¹ ⬝ q := /-(λx, x = a3)-/
+  by cases p; cases q; exact idpo
+
+  definition pathover_eq_r (p : a2 = a3) (q : a1 = a2) : q =[p] q ⬝ p := /-(λx, a1 = x)-/
+  by cases p; cases q; exact idpo
+
+  definition pathover_eq_lr (p : a1 = a2) (q : a1 = a1) : q =[p] p⁻¹ ⬝ q ⬝ p := /-(λx, x = x)-/
+  by cases p; rewrite [▸*,idp_con]; exact idpo
+
+  definition pathover_eq_Fl (p : a1 = a2) (q : f a1 = b) : q =[p] (ap f p)⁻¹ ⬝ q := /-(λx, f x = b)-/
+  by cases p; cases q; exact idpo
+
+  definition pathover_eq_Fr (p : a1 = a2) (q : b = f a1) : q =[p] q ⬝ (ap f p) := /-(λx, b = f x)-/
+  by cases p; exact idpo
+
+  definition pathover_eq_FlFr (p : a1 = a2) (q : f a1 = g a1) : q =[p] (ap f p)⁻¹ ⬝ q ⬝ (ap g p) :=
+  /-(λx, f x = g x)-/
+  by cases p; rewrite [▸*,idp_con]; exact idpo
+
+  definition pathover_eq_FlFr_D {B : A → Type} {f g : Πa, B a} (p : a1 = a2) (q : f a1 = g a1)
+    : q =[p] (apd f p)⁻¹ ⬝ ap (transport B p) q ⬝ (apd g p) := /-(λx, f x = g x)-/
+  by cases p; rewrite [▸*,idp_con,ap_id];exact idpo
+
+  definition pathover_eq_FFlr (p : a1 = a2) (q : h (f a1) = a1) : q =[p] (ap h (ap f p))⁻¹ ⬝ q ⬝ p :=
+  /-(λx, h (f x) = x)-/
+  by cases p; rewrite [▸*,idp_con];exact idpo
+
+  definition pathover_eq_lFFr (p : a1 = a2) (q : a1 = h (f a1)) : q =[p] p⁻¹ ⬝ q ⬝ (ap h (ap f p)) :=
+  /-(λx, x = h (f x))-/
+  by cases p; rewrite [▸*,idp_con];exact idpo
 
   -- The Functorial action of paths is [ap].
 
@@ -151,7 +156,7 @@ namespace eq
               (λq, by cases p;cases q;exact idp)
   local attribute is_equiv_concat_left [instance]
 
-  definition equiv_eq_closed_left (p : a1 = a2) (a3 : A) : (a1 = a3) ≃ (a2 = a3) :=
+  definition equiv_eq_closed_left (a3 : A) (p : a1 = a2) : (a1 = a3) ≃ (a2 = a3) :=
   equiv.mk (concat p⁻¹) _
 
   definition is_equiv_concat_right [instance] (p : a2 = a3) (a1 : A)
@@ -162,11 +167,11 @@ namespace eq
               (λq, by cases p;cases q;exact idp)
   local attribute is_equiv_concat_right [instance]
 
-  definition equiv_eq_closed_right (p : a2 = a3) (a1 : A) : (a1 = a2) ≃ (a1 = a3) :=
+  definition equiv_eq_closed_right (a1 : A) (p : a2 = a3) : (a1 = a2) ≃ (a1 = a3) :=
   equiv.mk (λq, q ⬝ p) _
 
   definition eq_equiv_eq_closed (p : a1 = a2) (q : a3 = a4) : (a1 = a3) ≃ (a2 = a4) :=
-  equiv.trans (equiv_eq_closed_left p a3) (equiv_eq_closed_right q a2)
+  equiv.trans (equiv_eq_closed_left a3 p) (equiv_eq_closed_right a2 q)
 
   definition is_equiv_whisker_left (p : a1 = a2) (q r : a2 = a3)
   : is_equiv (@whisker_left A a1 a2 a3 p q r) :=
@@ -179,10 +184,10 @@ namespace eq
       apply concat2,
         {apply concat, {apply whisker_left_con_right},
           apply concat2,
-            {cases p, cases q, apply idp},
+            {cases p, cases q, exact idp},
-            {apply idp}},
+            {exact idp}},
-        {cases p, cases r, apply idp}},
+        {cases p, cases r, exact idp}},
-    {intro s, cases s, cases q, cases p, apply idp}
+    {intro s, cases s, cases q, cases p, exact idp}
   end
 
   definition eq_equiv_con_eq_con_left (p : a1 = a2) (q r : a2 = a3) : (q = r) ≃ (p ⬝ q = p ⬝ r) :=
@@ -266,6 +271,44 @@ namespace eq
     : (q ⬝ p⁻¹ = r) ≃ (q = r ⬝ p) :=
   equiv.mk _ !is_equiv_eq_con_of_con_inv_eq
 
+  /- Pathover Equivalences -/
+
+  definition pathover_eq_equiv_l (p : a1 = a2) (q : a1 = a3) (r : a2 = a3) : q =[p] r ≃ q = p ⬝ r :=
+  /-(λx, x = a3)-/
+  by cases p; exact !pathover_idp ⬝e !equiv_eq_closed_right !idp_con⁻¹
+
+  definition pathover_eq_equiv_r (p : a2 = a3) (q : a1 = a2) (r : a1 = a3) : q =[p] r ≃ q ⬝ p = r :=
+  /-(λx, a1 = x)-/
+  by cases p; apply pathover_idp
+
+  definition pathover_eq_equiv_lr (p : a1 = a2) (q : a1 = a1) (r : a2 = a2)
+    : q =[p] r ≃ q ⬝ p = p ⬝ r := /-(λx, x = x)-/
+  by cases p; exact !pathover_idp ⬝e !equiv_eq_closed_right !idp_con⁻¹
+
+  definition pathover_eq_equiv_Fl (p : a1 = a2) (q : f a1 = b) (r : f a2 = b)
+    : q =[p] r ≃ q = ap f p ⬝ r := /-(λx, f x = b)-/
+  by cases p; exact !pathover_idp ⬝e !equiv_eq_closed_right !idp_con⁻¹
+
+  definition pathover_eq_equiv_Fr (p : a1 = a2) (q : b = f a1) (r : b = f a2)
+    : q =[p] r ≃ q ⬝ ap f p = r := /-(λx, b = f x)-/
+  by cases p; apply pathover_idp
+
+  definition pathover_eq_equiv_FlFr (p : a1 = a2) (q : f a1 = g a1) (r : f a2 = g a2)
+    : q =[p] r ≃ q ⬝ ap g p = ap f p ⬝ r := /-(λx, f x = g x)-/
+  by cases p; exact !pathover_idp ⬝e !equiv_eq_closed_right !idp_con⁻¹
+
+  definition pathover_eq_equiv_FFlr (p : a1 = a2) (q : h (f a1) = a1) (r : h (f a2) = a2)
+    : q =[p] r ≃ q ⬝ p = ap h (ap f p) ⬝ r :=
+  /-(λx, h (f x) = x)-/
+  by cases p; exact !pathover_idp ⬝e !equiv_eq_closed_right !idp_con⁻¹
+
+  definition pathover_eq_equiv_lFFr (p : a1 = a2) (q : a1 = h (f a1)) (r : a2 = h (f a2))
+    : q =[p] r ≃ q ⬝ ap h (ap f p) = p ⬝ r :=
+  /-(λx, x = h (f x))-/
+  by cases p; exact !pathover_idp ⬝e !equiv_eq_closed_right !idp_con⁻¹
+
   -- a lot of this library still needs to be ported from Coq HoTT
 
+
+
 end eq

hott/types/fiber.hlean

@@ -36,10 +36,7 @@ namespace fiber
       {apply equiv.symm, apply equiv_sigma_eq},
     apply sigma_equiv_sigma_id,
     intro p,
-    apply equiv_of_equiv_of_eq,
+    apply pathover_eq_equiv_Fl,
-    rotate 1,
-    apply inv_con_eq_equiv_eq_con,
-    {apply (ap (λx, x = _)), rewrite transport_eq_Fl}
   end
 
   definition fiber_eq {x y : fiber f b} (p : point x = point y)

hott/types/hprop_trunc.hlean

@@ -44,7 +44,7 @@ namespace is_trunc
       { apply equiv.to_is_equiv, apply is_contr.sigma_char},
       apply (@is_hprop.mk), intros,
       fapply sigma_eq, {apply x.2},
-      apply (@is_hprop.elim)},
+      apply (@is_hprop.elimo)},
     { intro A,
       apply is_trunc_is_equiv_closed,
       apply equiv.to_is_equiv,

hott/types/pi.hlean

@@ -3,13 +3,13 @@ Copyright (c) 2014-15 Floris van Doorn. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Author: Floris van Doorn
 
-Ported from Coq HoTT
+Partially ported from Coq HoTT
 Theorems about pi-types (dependent function spaces)
 -/
 
 import types.sigma
 
-open eq equiv is_equiv funext
+open eq equiv is_equiv funext sigma
 
 namespace pi
   variables {A A' : Type} {B : A → Type} {B' : A' → Type} {C : Πa, B a → Type}
@@ -59,6 +59,26 @@ namespace pi
     : (transport (λa, Π(b : A'), C a b) p f) b = transport (λa, C a b) p (f b) :=
   eq.rec_on p idp
 
+  /- Pathovers -/
+
+  definition pi_pathover {f : Πb, C a b} {g : Πb', C a' b'} {p : a = a'}
+    (r : Π(b : B a) (b' : B a') (q : b =[p] b'), f b =[apo011 C p q] g b') : f =[p] g :=
+  begin
+    cases p, apply pathover_idp_of_eq,
+    apply eq_of_homotopy, intro b,
+    apply eq_of_pathover_idp, apply r
+  end
+
+  definition pi_pathover' {C : (Σa, B a) → Type} {f : Πb, C ⟨a, b⟩} {g : Πb', C ⟨a', b'⟩}
+    {p : a = a'} (r : Π(b : B a) (b' : B a') (q : pathover B b p b'), f b =[dpair_eq_dpair p q] g b')
+    : f =[p] g :=
+  begin
+    cases p, apply pathover_idp_of_eq,
+    apply eq_of_homotopy, intro b,
+    apply (@eq_of_pathover_idp _ C), exact (r b b (pathover.idpatho b)),
+  end
+
+
   /- Maps on paths -/
 
   /- The action of maps given by lambda. -/
@@ -91,7 +111,8 @@ namespace pi
   (Π(b : B a), transportD B (λ(a : A) (b : B a), C ⟨a, b⟩) p b (f b) = g (transport B p b)) -/
   definition heq_pi_sigma {C : (Σa, B a) → Type} (p : a = a')
     (f : Π(b : B a), C ⟨a, b⟩) (g : Π(b' : B a'), C ⟨a', b'⟩) :
-    (Π(b : B a), (sigma_eq p idp) ▸ (f b) = g (p ▸ b)) ≃ (Π(b : B a), p ▸D (f b) = g (p ▸ b)) :=
+    (Π(b : B a), (sigma_eq p !pathover_tr) ▸ (f b) = g (p ▸ b)) ≃
+    (Π(b : B a), p ▸D (f b) = g (p ▸ b)) :=
   eq.rec_on p (λg, !equiv.refl) g
   end
 

hott/types/sigma.hlean

@@ -3,7 +3,7 @@ Copyright (c) 2014-15 Floris van Doorn. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Author: Floris van Doorn
 
-Ported from Coq HoTT
+Partially ported from Coq HoTT
 Theorems about sigma-types (dependent sums)
 -/
 
@@ -26,11 +26,11 @@ namespace sigma
   definition eta3 : Π (u : Σa b c, D a b c), ⟨u.1, u.2.1, u.2.2.1, u.2.2.2⟩ = u
   | eta3 ⟨u₁, u₂, u₃, u₄⟩ := idp
 
-  definition dpair_eq_dpair (p : a = a') (q : p ▸ b = b') : ⟨a, b⟩ = ⟨a', b'⟩ :=
+  definition dpair_eq_dpair (p : a = a') (q : b =[p] b') : ⟨a, b⟩ = ⟨a', b'⟩ :=
-  by cases p; cases q; reflexivity
+  by cases q; reflexivity
 
-  definition sigma_eq (p : u.1 = v.1) (q : p ▸ u.2 = v.2) : u = v :=
+  definition sigma_eq (p : u.1 = v.1) (q : u.2 =[p] v.2) : u = v :=
-  by cases u; cases v; apply (dpair_eq_dpair p q)
+  by cases u; cases v; exact (dpair_eq_dpair p q)
 
   /- Projections of paths from a total space -/
 
@@ -39,104 +39,104 @@ namespace sigma
 
   postfix `..1`:(max+1) := eq_pr1
 
-  definition eq_pr2 (p : u = v) : p..1 ▸ u.2 = v.2 :=
+  definition eq_pr2 (p : u = v) : u.2 =[p..1] v.2 :=
-  by cases p; reflexivity
+  by cases p; exact idpo
 
   postfix `..2`:(max+1) := eq_pr2
 
-  private definition dpair_sigma_eq (p : u.1 = v.1) (q : p ▸ u.2 = v.2)
+  private definition dpair_sigma_eq (p : u.1 = v.1) (q : u.2 =[p] v.2)
-      : ⟨(sigma_eq p q)..1, (sigma_eq p q)..2⟩ = ⟨p, q⟩ :=
+    : ⟨(sigma_eq p q)..1, (sigma_eq p q)..2⟩ = ⟨p, q⟩ :=
-  by cases u; cases v; cases p; cases q; apply idp
+  by cases u; cases v; cases q; apply idp
 
-  definition sigma_eq_pr1 (p : u.1 = v.1) (q : p ▸ u.2 = v.2) : (sigma_eq p q)..1 = p :=
+  definition sigma_eq_pr1 (p : u.1 = v.1) (q : u.2 =[p] v.2) : (sigma_eq p q)..1 = p :=
   (dpair_sigma_eq p q)..1
 
-  definition sigma_eq_pr2 (p : u.1 = v.1) (q : p ▸ u.2 = v.2)
+  definition sigma_eq_pr2 (p : u.1 = v.1) (q : u.2 =[p] v.2)
-      : sigma_eq_pr1 p q ▸ (sigma_eq p q)..2 = q :=
+    : (sigma_eq p q)..2 =[sigma_eq_pr1 p q] q :=
   (dpair_sigma_eq p q)..2
 
   definition sigma_eq_eta (p : u = v) : sigma_eq (p..1) (p..2) = p :=
   by cases p; cases u; reflexivity
 
-  definition tr_pr1_sigma_eq {B' : A → Type} (p : u.1 = v.1) (q : p ▸ u.2 = v.2)
+  definition tr_pr1_sigma_eq {B' : A → Type} (p : u.1 = v.1) (q : u.2 =[p] v.2)
-      : transport (λx, B' x.1) (sigma_eq p q) = transport B' p :=
+    : transport (λx, B' x.1) (sigma_eq p q) = transport B' p :=
-  by cases u; cases v; cases p; cases q; reflexivity
+  by cases u; cases v; cases q; reflexivity
 
   /- the uncurried version of sigma_eq. We will prove that this is an equivalence -/
 
-  definition sigma_eq_uncurried : Π (pq : Σ(p : u.1 = v.1), p ▸ u.2 = v.2), u = v
+  definition sigma_eq_unc : Π (pq : Σ(p : u.1 = v.1), u.2 =[p] v.2), u = v
-  | sigma_eq_uncurried ⟨pq₁, pq₂⟩ := sigma_eq pq₁ pq₂
+  | sigma_eq_unc ⟨pq₁, pq₂⟩ := sigma_eq pq₁ pq₂
 
-  definition dpair_sigma_eq_uncurried : Π (pq : Σ(p : u.1 = v.1), p ▸ u.2 = v.2),
+  definition dpair_sigma_eq_unc : Π (pq : Σ(p : u.1 = v.1), u.2 =[p] v.2),
-        ⟨(sigma_eq_uncurried pq)..1, (sigma_eq_uncurried pq)..2⟩ = pq
+    ⟨(sigma_eq_unc pq)..1, (sigma_eq_unc pq)..2⟩ = pq
-  | dpair_sigma_eq_uncurried ⟨pq₁, pq₂⟩ := dpair_sigma_eq pq₁ pq₂
+  | dpair_sigma_eq_unc ⟨pq₁, pq₂⟩ := dpair_sigma_eq pq₁ pq₂
 
-  definition sigma_eq_pr1_uncurried (pq : Σ(p : u.1 = v.1), p ▸ u.2 = v.2)
+  definition sigma_eq_pr1_unc (pq : Σ(p : u.1 = v.1), u.2 =[p] v.2)
-      : (sigma_eq_uncurried pq)..1 = pq.1 :=
+    : (sigma_eq_unc pq)..1 = pq.1 :=
-  (dpair_sigma_eq_uncurried pq)..1
+  (dpair_sigma_eq_unc pq)..1
 
-  definition sigma_eq_pr2_uncurried (pq : Σ(p : u.1 = v.1), p ▸ u.2 = v.2)
+  definition sigma_eq_pr2_unc (pq : Σ(p : u.1 = v.1), u.2 =[p] v.2) :
-      : (sigma_eq_pr1_uncurried pq) ▸ (sigma_eq_uncurried pq)..2 = pq.2 :=
+    (sigma_eq_unc pq)..2 =[sigma_eq_pr1_unc pq] pq.2 :=
-  (dpair_sigma_eq_uncurried pq)..2
+  (dpair_sigma_eq_unc pq)..2
 
-  definition sigma_eq_eta_uncurried (p : u = v) : sigma_eq_uncurried ⟨p..1, p..2⟩ = p :=
+  definition sigma_eq_eta_unc (p : u = v) : sigma_eq_unc ⟨p..1, p..2⟩ = p :=
   sigma_eq_eta p
 
-  definition tr_sigma_eq_pr1_uncurried {B' : A → Type}
+  definition tr_sigma_eq_pr1_unc {B' : A → Type}
-    (pq : Σ(p : u.1 = v.1), p ▸ u.2 = v.2)
+    (pq : Σ(p : u.1 = v.1), u.2 =[p] v.2)
-      : transport (λx, B' x.1) (@sigma_eq_uncurried A B u v pq) = transport B' pq.1 :=
+      : transport (λx, B' x.1) (@sigma_eq_unc A B u v pq) = transport B' pq.1 :=
   destruct pq tr_pr1_sigma_eq
 
   definition is_equiv_sigma_eq [instance] (u v : Σa, B a)
-      : is_equiv (@sigma_eq_uncurried A B u v) :=
+      : is_equiv (@sigma_eq_unc A B u v) :=
-  adjointify sigma_eq_uncurried
+  adjointify sigma_eq_unc
              (λp, ⟨p..1, p..2⟩)
-             sigma_eq_eta_uncurried
+             sigma_eq_eta_unc
-             dpair_sigma_eq_uncurried
+             dpair_sigma_eq_unc
 
-  definition equiv_sigma_eq (u v : Σa, B a) : (Σ(p : u.1 = v.1),  p ▸ u.2 = v.2) ≃ (u = v) :=
+  definition equiv_sigma_eq (u v : Σa, B a) : (Σ(p : u.1 = v.1),  u.2 =[p] v.2) ≃ (u = v) :=
-  equiv.mk sigma_eq_uncurried !is_equiv_sigma_eq
+  equiv.mk sigma_eq_unc !is_equiv_sigma_eq
 
-  definition dpair_eq_dpair_con (p1 : a  = a' ) (q1 : p1 ▸ b  = b' )
+  definition dpair_eq_dpair_con (p1 : a  = a' ) (q1 : b  =[p1] b' )
-                                  (p2 : a' = a'') (q2 : p2 ▸ b' = b'') :
+                                (p2 : a' = a'') (q2 : b' =[p2] b'') :
-      dpair_eq_dpair (p1 ⬝ p2) (con_tr p1 p2 b ⬝ ap (transport B p2) q1 ⬝ q2)
+    dpair_eq_dpair (p1 ⬝ p2) (q1 ⬝o q2) = dpair_eq_dpair p1 q1 ⬝ dpair_eq_dpair  p2 q2 :=
-    = dpair_eq_dpair p1 q1 ⬝ dpair_eq_dpair  p2 q2 :=
+  by cases q1; cases q2; reflexivity
-  by cases p1; cases p2; cases q1; cases q2; reflexivity
 
-  definition sigma_eq_con (p1 : u.1 = v.1) (q1 : p1 ▸ u.2 = v.2)
+  definition sigma_eq_con (p1 : u.1 = v.1) (q1 : u.2 =[p1] v.2)
-                              (p2 : v.1 = w.1) (q2 : p2 ▸ v.2 = w.2) :
+                          (p2 : v.1 = w.1) (q2 : v.2 =[p2] w.2) :
-      sigma_eq (p1 ⬝ p2) (con_tr p1 p2 u.2 ⬝ ap (transport B p2) q1 ⬝ q2)
+    sigma_eq (p1 ⬝ p2) (q1 ⬝o q2) = sigma_eq p1 q1 ⬝ sigma_eq p2 q2 :=
-    = sigma_eq p1 q1 ⬝ sigma_eq p2 q2 :=
   by cases u; cases v; cases w; apply dpair_eq_dpair_con
 
   local attribute dpair_eq_dpair [reducible]
-  definition dpair_eq_dpair_con_idp (p : a = a') (q : p ▸ b = b') :
+  definition dpair_eq_dpair_con_idp (p : a = a') (q : b =[p] b') :
-      dpair_eq_dpair p q = dpair_eq_dpair p idp ⬝ dpair_eq_dpair idp q :=
+    dpair_eq_dpair p q = dpair_eq_dpair p !pathover_tr ⬝
-  by cases p; cases q; reflexivity
+    dpair_eq_dpair idp (pathover_idp_of_eq (tr_eq_of_pathover q)) :=
+  by cases q; reflexivity
 
   /- eq_pr1 commutes with the groupoid structure. -/
 
   definition eq_pr1_idp (u : Σa, B a)           : (refl u) ..1 = refl (u.1)      := idp
-  definition eq_pr1_con  (p : u = v) (q : v = w) : (p ⬝ q)  ..1 = (p..1) ⬝ (q..1) := !ap_con
+  definition eq_pr1_con (p : u = v) (q : v = w) : (p ⬝ q)  ..1 = (p..1) ⬝ (q..1) := !ap_con
-  definition eq_pr1_inv   (p : u = v)             : p⁻¹      ..1 = (p..1)⁻¹        := !ap_inv
+  definition eq_pr1_inv (p : u = v)             : p⁻¹      ..1 = (p..1)⁻¹        := !ap_inv
 
   /- Applying dpair to one argument is the same as dpair_eq_dpair with reflexivity in the first place. -/
 
-  definition ap_dpair (q : b₁ = b₂) : ap (sigma.mk a) q = dpair_eq_dpair idp q :=
+  definition ap_dpair (q : b₁ = b₂) :
+    ap (sigma.mk a) q = dpair_eq_dpair idp (pathover_idp_of_eq q) :=
   by cases q; reflexivity
 
   /- Dependent transport is the same as transport along a sigma_eq. -/
 
   definition transportD_eq_transport (p : a = a') (c : C a b) :
-      p ▸D c = transport (λu, C (u.1) (u.2)) (dpair_eq_dpair p idp) c :=
+      p ▸D c = transport (λu, C (u.1) (u.2)) (dpair_eq_dpair p !pathover_tr) c :=
   by cases p; reflexivity
 
-  definition sigma_eq_eq_sigma_eq {p1 q1 : a = a'} {p2 : p1 ▸ b = b'} {q2 : q1 ▸ b = b'}
+  definition sigma_eq_eq_sigma_eq {p1 q1 : a = a'} {p2 : b =[p1] b'} {q2 : b =[q1] b'}
-      (r : p1 = q1) (s : r ▸ p2 = q2) : sigma_eq p1 p2 = sigma_eq q1 q2 :=
+      (r : p1 = q1) (s : p2 =[r] q2) : sigma_eq p1 p2 = sigma_eq q1 q2 :=
-  by cases r; cases s; reflexivity
+  by cases s; reflexivity
 
   /- A path between paths in a total space is commonly shown component wise. -/
-  definition sigma_eq2 {p q : u = v} (r : p..1 = q..1) (s : r ▸ p..2 = q..2)
+  definition sigma_eq2 {p q : u = v} (r : p..1 = q..1) (s : p..2 =[r] q..2)
     : p = q :=
   begin
     revert q r s,
@@ -147,9 +147,7 @@ namespace sigma
       apply sigma_eq_eta,
   end
 
-  /- In Coq they often have to give u and v explicitly when using the following definition -/
+  definition sigma_eq2_unc {p q : u = v} (rs : Σ(r : p..1 = q..1), p..2 =[r] q..2) : p = q :=
-  definition sigma_eq2_uncurried {p q : u = v}
-      (rs : Σ(r : p..1 = q..1), transport (λx, transport B x u.2 = v.2) r p..2 = q..2) : p = q :=
   destruct rs sigma_eq2
 
   /- Transport -/
@@ -159,7 +157,7 @@ namespace sigma
   In particular, this indicates why `transport` alone cannot be fully defined by induction on the structure of types, although Id-elim/transportD can be (cf. Observational Type Theory).  A more thorough set of lemmas, along the lines of the present ones but dealing with Id-elim rather than just transport, might be nice to have eventually? -/
 
   definition transport_eq (p : a = a') (bc : Σ(b : B a), C a b)
-      : p ▸ bc = ⟨p ▸ bc.1, p ▸D bc.2⟩ :=
+    : p ▸ bc = ⟨p ▸ bc.1, p ▸D bc.2⟩ :=
   by cases p; cases bc; reflexivity
 
   /- The special case when the second variable doesn't depend on the first is simpler. -/
@@ -175,72 +173,68 @@ namespace sigma
     cases p, cases bcd with b cd, cases cd, reflexivity
   end
 
+  /- Pathovers -/
+
+  definition eta_pathover (p : a = a') (bc : Σ(b : B a), C a b)
+    : bc =[p] ⟨p ▸ bc.1, p ▸D bc.2⟩ :=
+  by cases p; cases bc; apply idpo
+
+  definition sigma_pathover (p : a = a') (u : Σ(b : B a), C a b) (v : Σ(b : B a'), C a' b)
+    (r : u.1 =[p] v.1) (s : u.2 =[apo011 C p r] v.2) : u =[p] v :=
+  begin cases u, cases v, cases r, esimp [apo011] at s, induction s using idp_rec_on, apply idpo end
+
+  /- TODO:
+    * define the projections from the type u =[p] v
+    * show that the uncurried version of sigma_pathover is an equivalence
+  -/
+
   /- Functorial action -/
   variables (f : A → A') (g : Πa, B a → B' (f a))
 
-  definition sigma_functor (u : Σa, B a) : Σa', B' a' :=
+  definition sigma_functor [unfold-c 7] (u : Σa, B a) : Σa', B' a' :=
   ⟨f u.1, g u.1 u.2⟩
 
   /- Equivalences -/
-
   definition is_equiv_sigma_functor [H1 : is_equiv f] [H2 : Π a, is_equiv (g a)]
       : is_equiv (sigma_functor f g) :=
   adjointify (sigma_functor f g)
              (sigma_functor f⁻¹ (λ(a' : A') (b' : B' a'),
                ((g (f⁻¹ a'))⁻¹ (transport B' (right_inv f a')⁻¹ b'))))
   begin
-    intro u',
+    intro u', cases u' with a' b',
-    cases u' with a' b',
     apply sigma_eq (right_inv f a'),
-  --   rewrite right_inv,
+    rewrite [▸*,right_inv (g (f⁻¹ a')),▸*],
-  -- end
+    apply tr_pathover
-    -- "rewrite right_inv (g (f⁻¹ a'))"
-    apply concat, apply (ap (λx, (transport B' (right_inv f a') x))), apply (right_inv (g (f⁻¹ a'))),
-    show right_inv f a' ▸ ((right_inv f a')⁻¹ ▸ b') = b',
-    from tr_inv_tr (right_inv f a') b'
   end
   begin
     intro u,
     cases u with a b,
     apply (sigma_eq (left_inv f a)),
-    calc
+    apply pathover_of_tr_eq,
-      transport B (left_inv f a) ((g (f⁻¹ (f a)))⁻¹ (transport B' (right_inv f (f a))⁻¹ (g a b)))
+    rewrite [▸*,adj f,-(fn_tr_eq_tr_fn (left_inv f a) (λ a, (g a)⁻¹)),
-          = (g a)⁻¹ (transport (B' ∘ f) (left_inv f a) (transport B' (right_inv f (f a))⁻¹ (g a b)))
+             ▸*,transport_compose B' f,tr_inv_tr,left_inv]
-              : by esimp; rewrite (fn_tr_eq_tr_fn (left_inv f a) (λ a, (g a)⁻¹))
-      ... = (g a)⁻¹ (transport B' (ap f (left_inv f a)) (transport B' (right_inv f (f a))⁻¹ (g a b)))
-              : ap (g a)⁻¹ !transport_compose
-      ... = (g a)⁻¹ (transport B' (ap f (left_inv f a)) (transport B' (ap f (left_inv f a))⁻¹ (g a b)))
-           : ap (λ x, (g a)⁻¹ (transport B' (ap f (left_inv f a)) (transport B' x⁻¹ (g a b)))) (adj f a)
-      ... = (g a)⁻¹ (g a b) : {!tr_inv_tr}
-      ... = b : by esimp; rewrite (left_inv (g a) b)
   end
 
   definition sigma_equiv_sigma_of_is_equiv [H1 : is_equiv f] [H2 : Π a, is_equiv (g a)]
     : (Σa, B a) ≃ (Σa', B' a') :=
   equiv.mk (sigma_functor f g) !is_equiv_sigma_functor
 
-  section
-  local attribute inv [irreducible]
-  local attribute function.compose [irreducible] --this is needed for the following class inference problem
   definition sigma_equiv_sigma (Hf : A ≃ A') (Hg : Π a, B a ≃ B' (to_fun Hf a)) :
       (Σa, B a) ≃ (Σa', B' a') :=
   sigma_equiv_sigma_of_is_equiv (to_fun Hf) (λ a, to_fun (Hg a))
-  end
 
   definition sigma_equiv_sigma_id {B' : A → Type} (Hg : Π a, B a ≃ B' a) : (Σa, B a) ≃ Σa, B' a :=
   sigma_equiv_sigma equiv.refl Hg
 
-  definition ap_sigma_functor_eq_dpair (p : a = a') (q : p ▸ b = b')
+  definition ap_sigma_functor_eq_dpair (p : a = a') (q : b =[p] b') :
-    : ap (sigma.sigma_functor f g) (sigma_eq p q)
+    ap (sigma_functor f g) (sigma_eq p q) = sigma_eq (ap f p) (pathover.rec_on q idpo) :=
-    = sigma_eq (ap f p)
+  by cases q; reflexivity
-                 ((transport_compose _ f p (g a b))⁻¹ ⬝ (fn_tr_eq_tr_fn p g b)⁻¹ ⬝ ap (g a') q) :=
-  by cases p; cases q; reflexivity
 
-  definition ap_sigma_functor_eq (p : u.1 = v.1) (q : p ▸ u.2 = v.2)
+  -- definition ap_sigma_functor_eq (p : u.1 = v.1) (q : u.2 =[p] v.2)
-    : ap (sigma.sigma_functor f g) (sigma_eq p q) =
+  --   : ap (sigma_functor f g) (sigma_eq p q) =
-      sigma_eq (ap f p)
+  --     sigma_eq (ap f p)
-       ((transport_compose B' f p (g u.1 u.2))⁻¹ ⬝ (fn_tr_eq_tr_fn p g u.2)⁻¹ ⬝ ap (g v.1) q) :=
+  --      ((transport_compose B' f p (g u.1 u.2))⁻¹ ⬝ (fn_tr_eq_tr_fn p g u.2)⁻¹ ⬝ ap (g v.1) q) :=
-  by cases u; cases v; apply ap_sigma_functor_eq_dpair
+  -- by cases u; cases v; apply ap_sigma_functor_eq_dpair
 
   /- definition 3.11.9(i): Summing up a contractible family of types does nothing. -/
   open is_trunc
@@ -249,7 +243,7 @@ namespace sigma
   adjointify pr1
              (λa, ⟨a, !center⟩)
              (λa, idp)
-             (λu, sigma_eq idp !center_eq)
+             (λu, sigma_eq idp (pathover_idp_of_eq !center_eq))
 
   definition sigma_equiv_of_is_contr_pr2 [H : Π a, is_contr (B a)] : (Σa, B a) ≃ A :=
   equiv.mk pr1 _
@@ -262,7 +256,7 @@ namespace sigma
     (λu, (center_eq u.1)⁻¹ ▸ u.2)
     (λb, ⟨!center, b⟩)
     (λb, ap (λx, x ▸ b) !hprop_eq_of_is_contr)
-    (λu, sigma_eq !center_eq !tr_inv_tr))
+    (λu, sigma_eq !center_eq !tr_pathover))
 
   /- Associativity -/
 
@@ -284,7 +278,7 @@ namespace sigma
 
   /- Symmetry -/
 
-  definition comm_equiv_uncurried (C : A × A' → Type) : (Σa a', C (a, a')) ≃ (Σa' a, C (a, a')) :=
+  definition comm_equiv_unc (C : A × A' → Type) : (Σa a', C (a, a')) ≃ (Σa' a, C (a, a')) :=
   calc
     (Σa a', C (a, a')) ≃ Σu, C u : assoc_equiv_prod
                  ... ≃ Σv, C (flip v) : sigma_equiv_sigma !prod_comm_equiv
@@ -292,7 +286,7 @@ namespace sigma
                  ... ≃ (Σa' a, C (a, a')) : assoc_equiv_prod
 
   definition sigma_comm_equiv (C : A → A' → Type) : (Σa a', C a a') ≃ (Σa' a, C a a') :=
-  comm_equiv_uncurried (λu, C (prod.pr1 u) (prod.pr2 u))
+  comm_equiv_unc (λu, C (prod.pr1 u) (prod.pr2 u))
 
   definition equiv_prod (A B : Type) : (Σ(a : A), B) ≃ A × B :=
   equiv.mk _ (adjointify
@@ -323,30 +317,30 @@ namespace sigma
 
   /- *** The negative universal property. -/
 
-  protected definition coind_uncurried (fg : Σ(f : Πa, B a), Πa, C a (f a)) (a : A)
+  protected definition coind_unc (fg : Σ(f : Πa, B a), Πa, C a (f a)) (a : A)
     : Σ(b : B a), C a b :=
   ⟨fg.1 a, fg.2 a⟩
 
   protected definition coind (f : Π a, B a) (g : Π a, C a (f a)) (a : A) : Σ(b : B a), C a b :=
-  sigma.coind_uncurried ⟨f, g⟩ a
+  sigma.coind_unc ⟨f, g⟩ a
 
   --is the instance below dangerous?
   --in Coq this can be done without function extensionality
   definition is_equiv_coind [instance] (C : Πa, B a → Type)
-    : is_equiv (@sigma.coind_uncurried _ _ C) :=
+    : is_equiv (@sigma.coind_unc _ _ C) :=
   adjointify _ (λ h, ⟨λa, (h a).1, λa, (h a).2⟩)
                (λ h, proof eq_of_homotopy (λu, !sigma.eta) qed)
                (λfg, destruct fg (λ(f : Π (a : A), B a) (g : Π (x : A), C x (f x)), proof idp qed))
 
   definition sigma_pi_equiv_pi_sigma : (Σ(f : Πa, B a), Πa, C a (f a)) ≃ (Πa, Σb, C a b) :=
-  equiv.mk sigma.coind_uncurried _
+  equiv.mk sigma.coind_unc _
   end
 
   /- ** Subtypes (sigma types whose second components are hprops) -/
 
   /- To prove equality in a subtype, we only need equality of the first component. -/
   definition subtype_eq [H : Πa, is_hprop (B a)] (u v : Σa, B a) : u.1 = v.1 → u = v :=
-  (sigma_eq_uncurried ∘ (@inv _ _ pr1 (@is_equiv_pr1 _ _ (λp, !is_trunc.is_trunc_eq))))
+  sigma_eq_unc ∘ inv pr1
 
   definition is_equiv_subtype_eq [H : Πa, is_hprop (B a)] (u v : Σa, B a)
       : is_equiv (subtype_eq u v) :=
@@ -361,20 +355,12 @@ namespace sigma
       [HA : is_trunc n A] [HB : Πa, is_trunc n (B a)] : is_trunc n (Σa, B a) :=
   begin
   revert A B HA HB,
-  eapply (trunc_index.rec_on n),
+  induction n with n IH,
-    intro A B HA HB,
+  { intro A B HA HB, fapply is_trunc_equiv_closed_rev, apply sigma_equiv_of_is_contr_pr1},
-      fapply is_trunc.is_trunc_equiv_closed,
+  { intro A B HA HB, apply is_trunc_succ_intro, intro u v,
-        symmetry,
+    apply is_trunc_equiv_closed,
-          apply sigma_equiv_of_is_contr_pr1,
+      apply equiv_sigma_eq,
-     intro n IH A B HA HB,
+      exact IH _ _ _ _}
-       fapply is_trunc.is_trunc_succ_intro, intro u v,
-      fapply is_trunc.is_trunc_equiv_closed,
-         apply equiv_sigma_eq,
-         apply IH,
-           apply is_trunc.is_trunc_eq,
-           intro p,
-             show is_trunc n (p ▸ u .2 = v .2), from
-             is_trunc.is_trunc_eq n (p ▸ u.2) (v.2),
   end
 
 end sigma

hott/types/types.md

@@ -9,6 +9,7 @@ Various datatypes.
 * [pi](pi.hlean)
 * [arrow](arrow.hlean)
 * [eq](eq.hlean)
+* [square](square.hlean): type of squares in a type
 * [fiber](fiber.hlean)
 * [hprop_trunc](hprop_trunc.hlean): in this file we prove that `is_trunc n A` is a mere proposition. We separate this from [trunc](trunc.hlean) to avoid circularity in imports.
 * [equiv](equiv.hlean)