feat(hott): various minor changes in the HoTT library

hott/algebra/category/constructions/functor.hlean

@@ -123,7 +123,6 @@ namespace category
       {intro c c' f,
         esimp [eq_of_iso_ob, inv_of_eq, hom_of_eq, eq_of_iso],
         rewrite [*right_inv iso_of_eq],
-        esimp [function.id],
         symmetry, apply @naturality_iso _ _ _ _ _ (iso.struct _)
       }
     end

hott/algebra/category/constructions/hset.hlean

@@ -35,8 +35,8 @@ namespace category
     definition equiv_of_iso {A B : Precategory_hset} (f : A ≅ B) : A ≃ B :=
     begin
       apply equiv.MK (to_hom f) (iso.to_inv f),
-       exact ap10 (right_inverse (to_hom f)),
+        exact ap10 (to_right_inverse f),
-       exact ap10 (left_inverse  (to_hom f))
+        exact ap10 (to_left_inverse f)
     end
 
     definition is_equiv_iso_of_equiv (A B : Precategory_hset) : is_equiv (@iso_of_equiv A B) :=
@@ -64,8 +64,8 @@ namespace category
     equiv.MK (λf, iso_of_equiv f)
              (λf, proof equiv.MK (to_hom f)
                            (iso.to_inv f)
-                           (ap10 (right_inverse (to_hom f)))
+                           (ap10 (to_right_inverse f))
-                           (ap10 (left_inverse  (to_hom f))) qed)
+                           (ap10 (to_left_inverse  f)) qed)
              (λf, proof iso_eq idp qed)
              (λf, proof equiv_eq idp qed)
 

hott/algebra/category/iso.hlean

@@ -137,24 +137,27 @@ namespace iso
   include C
 
   infix `≅`:50 := iso
-  attribute iso.struct [instance] [priority 400]
+  attribute struct [instance] [priority 400]
 
   attribute to_hom [coercion]
 
   protected definition MK [constructor] (f : a ⟶ b) (g : b ⟶ a)
     (H1 : g ∘ f = id) (H2 : f ∘ g = id) :=
-  @mk _ _ _ _ f (is_iso.mk H1 H2)
+  @(mk f) (is_iso.mk H1 H2)
 
-  definition to_inv [unfold 5] (f : a ≅ b) : b ⟶ a :=
+  definition to_inv [unfold 5] (f : a ≅ b) : b ⟶ a := (to_hom f)⁻¹
-  (to_hom f)⁻¹
+  definition to_left_inverse  [unfold 5] (f : a ≅ b) : (to_hom f)⁻¹ ∘ (to_hom f) = id :=
+  left_inverse  (to_hom f)
+  definition to_right_inverse [unfold 5] (f : a ≅ b) : (to_hom f) ∘ (to_hom f)⁻¹ = id :=
+  right_inverse (to_hom f)
 
   protected definition refl [constructor] (a : ob) : a ≅ a :=
   mk (ID a)
 
-  protected definition symm ⦃a b : ob⦄ (H : a ≅ b) : b ≅ a :=
+  protected definition symm [constructor] ⦃a b : ob⦄ (H : a ≅ b) : b ≅ a :=
   mk (to_hom H)⁻¹
 
-  protected definition trans ⦃a b c : ob⦄ (H1 : a ≅ b) (H2 : b ≅ c) : a ≅ c :=
+  protected definition trans [constructor] ⦃a b c : ob⦄ (H1 : a ≅ b) (H2 : b ≅ c) : a ≅ c :=
   mk (to_hom H2 ∘ to_hom H1)
 
   definition iso_mk_eq {f f' : a ⟶ b} [H : is_iso f] [H' : is_iso f'] (p : f = f')

hott/algebra/e_closure.hlean

@@ -33,7 +33,7 @@ section
 
   variables ⦃a a' : A⦄ {s : R a a'} {r : T a a}
   parameter {R}
-  protected definition e_closure.elim {B : Type} {f : A → B}
+  protected definition e_closure.elim [unfold 6] {B : Type} {f : A → B}
     (e : Π⦃a a' : A⦄, R a a' → f a = f a') (t : T a a') : f a = f a' :=
   begin
     induction t,
@@ -43,7 +43,7 @@ section
       exact v_0 ⬝ v_1
   end
 
-  definition ap_e_closure_elim_h {B C : Type} {f : A → B} {g : B → C}
+  definition ap_e_closure_elim_h [unfold 12] {B C : Type} {f : A → B} {g : B → C}
     (e : Π⦃a a' : A⦄, R a a' → f a = f a')
     {e' : Π⦃a a' : A⦄, R a a' → g (f a) = g (f a')}
     (p : Π⦃a a' : A⦄ (s : R a a'), ap g (e s) = e' s) (t : T a a')
@@ -84,16 +84,14 @@ section
              (ap_e_closure_elim_h e' (λa a' s, (ap (ap h) (p s))⁻¹) t) :=
   begin
     induction t,
-    { unfold [ap_e_closure_elim_h, e_closure.elim],
+    { esimp,
       apply square_of_eq, exact !con.right_inv ⬝ !con.left_inv⁻¹},
     { apply ids},
-    { unfold [e_closure.elim, ap_e_closure_elim_h],
+    { rewrite [▸*,ap_con (ap h)],
-      rewrite [ap_con (ap h)],
       refine (transpose !ap_compose_inv)⁻¹ᵛ ⬝h _,
       rewrite [con_inv,inv_inv,-inv2_inv],
       exact !ap_inv2 ⬝v square_inv2 v_0},
-    { unfold [e_closure.elim, ap_e_closure_elim_h],
+    { rewrite [▸*,ap_con (ap h)],
-      rewrite [ap_con (ap h)],
       refine (transpose !ap_compose_con)⁻¹ᵛ ⬝h _,
       rewrite [con_inv,inv_inv,con2_inv],
       refine !ap_con2 ⬝v square_con2 v_0 v_1},

hott/arity.hlean

@@ -187,7 +187,7 @@ namespace funext
   adjointify _
              eq_of_homotopy2
              begin
-               intro H, esimp [apd100, eq_of_homotopy2, function.compose],
+               intro H, esimp [apd100, eq_of_homotopy2],
                apply eq_of_homotopy, intro a,
                apply concat, apply (ap (λx, apd10 (x a))), apply (right_inv apd10),
                apply (right_inv apd10)

hott/hit/circle.hlean

@@ -152,7 +152,7 @@ attribute circle.rec2 circle.elim2 [unfold 6] [recursor 6]
 attribute circle.elim2_type [unfold 5]
 attribute circle.rec2_on circle.elim2_on [unfold 2]
 attribute circle.elim2_type [unfold 1]
-attribute circle.elim circle.rec [unfold 4] [recursor 4]
+attribute circle.rec circle.elim [unfold 4] [recursor 4]
 attribute circle.elim_type [unfold 3]
 attribute circle.rec_on circle.elim_on [unfold 2]
 attribute circle.elim_type_on [unfold 1]

hott/hit/colimit.hlean

@@ -93,7 +93,7 @@ namespace seq_colim
 section
   /-
     we define it directly in terms of quotients. An alternative definition could be
-    definition seq_colim := colimit.colimit A function.id succ f
+    definition seq_colim := colimit.colimit A id succ f
   -/
   parameters {A : ℕ → Type} (f : Π⦃n⦄, A n → A (succ n))
   variables {n : ℕ} (a : A n)

hott/hit/susp.hlean

@@ -105,7 +105,7 @@ namespace susp
     { intro a, induction a,
       { reflexivity},
       { reflexivity},
-      { apply pathover_eq, apply hdeg_square,
+      { apply eq_pathover, apply hdeg_square,
         rewrite [▸*,ap_compose' _ (Susp_functor f),↑Susp_functor,+elim_merid]}},
     { reflexivity}
   end
@@ -136,7 +136,7 @@ namespace susp
       refine _ ⬝ !con.assoc',
       rewrite inverse2_right_inv,
       refine _ ⬝ !con.assoc',
-      rewrite [ap_con_right_inv,↑Susp_functor,idp_con_idp,-ap_compose]},
+      rewrite [ap_con_right_inv], unfold Susp_functor, xrewrite [idp_con_idp,-ap_compose], },
   end
 
   definition loop_susp_counit [constructor] (X : Pointed) : Susp (Ω X) →* X :=
@@ -154,9 +154,9 @@ namespace susp
     { intro x', induction x' with p,
       { reflexivity},
       { reflexivity},
-      { esimp, apply pathover_eq, apply hdeg_square,
+      { esimp, apply eq_pathover, apply hdeg_square,
-        xrewrite [ap_compose f,ap_compose (susp.elim (f x) (f x) (λ (a : f x = f x), a)),▸*,
+        xrewrite [ap_compose f,ap_compose (susp.elim (f x) (f x) (λ (a : f x = f x), a)),▸*],
-                  +elim_merid,▸*,idp_con]}},
+        xrewrite [+elim_merid,▸*,idp_con]}},
     { reflexivity}
   end
 
@@ -181,7 +181,7 @@ namespace susp
     { intro x', induction x',
       { reflexivity},
       { exact merid pt},
-      { apply pathover_eq,
+      { apply eq_pathover,
         xrewrite [▸*, ap_id, ap_compose (susp.elim north north (λa, a)), +elim_merid,▸*],
         apply square_of_eq, exact !idp_con ⬝ !inv_con_cancel_right⁻¹}},
     { reflexivity}

hott/hit/two_quotient.hlean

@@ -5,7 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Floris van Doorn
 -/
 
-import hit.circle types.eq2 algebra.e_closure
+import hit.circle types.eq2 algebra.e_closure types.cubical.cube
 
 open quotient eq circle sum sigma equiv function relation
 
@@ -21,17 +21,17 @@ namespace simple_two_quotient
 
   local abbreviation B := A ⊎ Σ(a : A) (r : T a a), Q r
 
-  inductive pre_simple_two_quotient_rel : B → B → Type :=
+  inductive pre_two_quotient_rel : B → B → Type :=
-  | pre_Rmk {} : Π⦃a a'⦄ (r : R a a'), pre_simple_two_quotient_rel (inl a) (inl a')
+  | pre_Rmk {} : Π⦃a a'⦄ (r : R a a'), pre_two_quotient_rel (inl a) (inl a')
   --BUG: if {} not provided, the alias for pre_Rmk is wrong
 
-  definition pre_simple_two_quotient := quotient pre_simple_two_quotient_rel
+  definition pre_two_quotient := quotient pre_two_quotient_rel
 
-  open pre_simple_two_quotient_rel
+  open pre_two_quotient_rel
-  local abbreviation C := quotient pre_simple_two_quotient_rel
+  local abbreviation C := quotient pre_two_quotient_rel
-  protected definition j [constructor] (a : A) : C := class_of pre_simple_two_quotient_rel (inl a)
+  protected definition j [constructor] (a : A) : C := class_of pre_two_quotient_rel (inl a)
   protected definition pre_aux [constructor] (q : Q r) : C :=
-  class_of pre_simple_two_quotient_rel (inr ⟨a, r, q⟩)
+  class_of pre_two_quotient_rel (inr ⟨a, r, q⟩)
   protected definition e (s : R a a') : j a = j a' := eq_of_rel _ (pre_Rmk s)
   protected definition et (t : T a a') : j a = j a' := e_closure.elim e t
   protected definition f [unfold 7] (q : Q r) : S¹ → C :=
@@ -102,7 +102,7 @@ namespace simple_two_quotient
   definition incl2 (q : Q r) : inclt r = idp :=
   inclt_eq_incltw r ⬝ incl2w q
 
-  local attribute simple_two_quotient f i incl0 aux incl1 incl2' inclt [reducible]
+  local attribute simple_two_quotient f i D incl0 aux incl1 incl2' inclt [reducible]
   local attribute i aux incl0 [constructor]
   protected definition elim {P : Type} (P0 : A → P)
     (P1 : Π⦃a a' : A⦄ (s : R a a'), P0 a = P0 a')
@@ -116,7 +116,7 @@ namespace simple_two_quotient
       { exact P1}},
     { exact abstract begin induction H, induction x,
       { exact idpath (P0 a)},
-      { unfold f, apply pathover_eq, apply hdeg_square,
+      { unfold f, apply eq_pathover, apply hdeg_square,
         exact abstract ap_compose (pre_elim P0 _ P1) (f q) loop ⬝
               ap _ !elim_loop ⬝
               !elim_et ⬝
@@ -167,7 +167,7 @@ namespace simple_two_quotient
     krewrite [-eq_of_homotopy3_inv,-eq_of_homotopy3_con]
   end
 
-  definition elim_incl2'_incl0 {P : Type} {P0 : A → P}
+  definition elim_incl2' {P : Type} {P0 : A → P}
     {P1 : Π⦃a a' : A⦄ (s : R a a'), P0 a = P0 a'}
     (P2 : Π⦃a : A⦄ ⦃r : T a a⦄ (q : Q r), e_closure.elim P1 r = idp)
     ⦃a : A⦄ ⦃r : T a a⦄ (q : Q r) : ap (elim P0 P1 P2) (incl2' q base) = idpath (P0 a) :=
@@ -198,7 +198,7 @@ namespace simple_two_quotient
     apply eq_vconcat,
     { apply ap (λx, _ ⬝ eq_con_inv_of_con_eq ((_ ⬝ x ⬝ _)⁻¹ ⬝ _) ⬝ _),
       transitivity _, apply ap eq_of_square,
-        apply to_right_inv !pathover_eq_equiv_square (hdeg_square (elim_1 P A R Q P0 P1 a r q P2)),
+        apply to_right_inv !eq_pathover_equiv_square (hdeg_square (elim_1 P A R Q P0 P1 a r q P2)),
       transitivity _, apply eq_of_square_hdeg_square,
       unfold elim_1, reflexivity},
     rewrite [+con_inv,whisker_left_inv,+inv_inv,-whisker_right_inv,
@@ -212,10 +212,10 @@ namespace simple_two_quotient
              right_inv_eq_idp (
                (λ(x : ap (elim P0 P1 P2) (incl2' q base) = idpath
                (elim P0 P1 P2 (class_of simple_two_quotient_rel (f q base)))), x)
-                (elim_incl2'_incl0 P2 q)),
+                (elim_incl2' P2 q)),
              ↑[whisker_left]],
     xrewrite [con2_con_con2],
-    rewrite [idp_con,↑elim_incl2'_incl0,con.left_inv,whisker_right_inv,↑whisker_right],
+    rewrite [idp_con,↑elim_incl2',con.left_inv,whisker_right_inv,↑whisker_right],
     xrewrite [con.assoc _ _ (_ ◾ _)],
     rewrite [con.left_inv,▸*,-+con.assoc,con.assoc _⁻¹,↑[elim,function.compose],con.left_inv,
              ▸*,↑j,con.left_inv,idp_con],

hott/init/equiv.hlean

@@ -17,8 +17,8 @@ open eq function lift
 structure is_equiv [class] {A B : Type} (f : A → B) :=
 mk' ::
   (inv : B → A)
-  (right_inv : (f ∘ inv) ~ id)
+  (right_inv : Πb, f (inv b) = b)
-  (left_inv : (inv ∘ f) ~ id)
+  (left_inv : Πa, inv (f a) = a)
   (adj : Πx, right_inv (f x) = ap f (left_inv x))
 
 attribute is_equiv.inv [quasireducible]
@@ -66,44 +66,43 @@ namespace is_equiv
 
   section
   parameters {A B : Type} (f : A → B) (g : B → A)
-            (ret : f ∘ g ~ id) (sec : g ∘ f ~ id)
+            (ret : Πb, f (g b) = b) (sec : Πa, g (f a) = a)
 
-  private definition adjointify_sect' : g ∘ f ~ id :=
+  private definition adjointify_left_inv' (a : A) : g (f a) = a :=
-    (λx, ap g (ap f (inverse (sec x))) ⬝ ap g (ret (f x)) ⬝ sec x)
+  ap g (ap f (inverse (sec a))) ⬝ ap g (ret (f a)) ⬝ sec a
 
-  private definition adjointify_adj' : Π (x : A), ret (f x) = ap f (adjointify_sect' x) :=
+  private definition adjointify_adj' (a : A) : ret (f a) = ap f (adjointify_left_inv' a) :=
-    (λ (a : A),
+  let fgretrfa := ap f (ap g (ret (f a))) in
-      let fgretrfa := ap f (ap g (ret (f a))) in
+  let fgfinvsect := ap f (ap g (ap f (sec a)⁻¹)) in
-      let fgfinvsect := ap f (ap g (ap f (sec a)⁻¹)) in
+  let fgfa := f (g (f a)) in
-      let fgfa := f (g (f a)) in
+  let retrfa := ret (f a) in
-      let retrfa := ret (f a) in
+  have eq1 : ap f (sec a) = _,
-      have eq1 : ap f (sec a) = _,
+    from calc ap f (sec a)
-        from calc ap f (sec a)
+          = idp ⬝ ap f (sec a)                                     : by rewrite idp_con
-              = idp ⬝ ap f (sec a)                                     : by rewrite idp_con
+      ... = (ret (f a) ⬝ (ret (f a))⁻¹) ⬝ ap f (sec a)             : by rewrite con.right_inv
-          ... = (ret (f a) ⬝ (ret (f a))⁻¹) ⬝ ap f (sec a)             : by rewrite con.right_inv
+      ... = ((ret fgfa)⁻¹ ⬝ ap (f ∘ g) (ret (f a))) ⬝ ap f (sec a) : by rewrite con_ap_eq_con
-          ... = ((ret fgfa)⁻¹ ⬝ ap (f ∘ g) (ret (f a))) ⬝ ap f (sec a) : by rewrite con_ap_eq_con
+      ... = ((ret fgfa)⁻¹ ⬝ fgretrfa) ⬝ ap f (sec a)               : by rewrite ap_compose
-          ... = ((ret fgfa)⁻¹ ⬝ fgretrfa) ⬝ ap f (sec a)               : by rewrite ap_compose
+      ... = (ret fgfa)⁻¹ ⬝ (fgretrfa ⬝ ap f (sec a))               : by rewrite con.assoc,
-          ... = (ret fgfa)⁻¹ ⬝ (fgretrfa ⬝ ap f (sec a))               : by rewrite con.assoc,
+  have eq2 : ap f (sec a) ⬝ idp = (ret fgfa)⁻¹ ⬝ (fgretrfa ⬝ ap f (sec a)),
-      have eq2 : ap f (sec a) ⬝ idp = (ret fgfa)⁻¹ ⬝ (fgretrfa ⬝ ap f (sec a)),
+    from !con_idp ⬝ eq1,
-        from !con_idp ⬝ eq1,
+  have eq3 : idp = _,
-      have eq3 : idp = _,
+    from calc idp
-        from calc idp
+          = (ap f (sec a))⁻¹ ⬝ ((ret fgfa)⁻¹ ⬝ (fgretrfa ⬝ ap f (sec a))) : eq_inv_con_of_con_eq eq2
-              = (ap f (sec a))⁻¹ ⬝ ((ret fgfa)⁻¹ ⬝ (fgretrfa ⬝ ap f (sec a))) : eq_inv_con_of_con_eq eq2
+      ... = ((ap f (sec a))⁻¹ ⬝ (ret fgfa)⁻¹) ⬝ (fgretrfa ⬝ ap f (sec a)) : by rewrite con.assoc'
-          ... = ((ap f (sec a))⁻¹ ⬝ (ret fgfa)⁻¹) ⬝ (fgretrfa ⬝ ap f (sec a)) : by rewrite con.assoc'
+      ... = (ap f (sec a)⁻¹ ⬝ (ret fgfa)⁻¹) ⬝ (fgretrfa ⬝ ap f (sec a))   : by rewrite ap_inv
-          ... = (ap f (sec a)⁻¹ ⬝ (ret fgfa)⁻¹) ⬝ (fgretrfa ⬝ ap f (sec a))   : by rewrite ap_inv
+      ... = ((ap f (sec a)⁻¹ ⬝ (ret fgfa)⁻¹) ⬝ fgretrfa) ⬝ ap f (sec a)   : by rewrite con.assoc'
-          ... = ((ap f (sec a)⁻¹ ⬝ (ret fgfa)⁻¹) ⬝ fgretrfa) ⬝ ap f (sec a)   : by rewrite con.assoc'
+      ... = ((retrfa⁻¹ ⬝ ap (f ∘ g) (ap f (sec a)⁻¹)) ⬝ fgretrfa) ⬝ ap f (sec a) : by rewrite con_ap_eq_con
-          ... = ((retrfa⁻¹ ⬝ ap (f ∘ g) (ap f (sec a)⁻¹)) ⬝ fgretrfa) ⬝ ap f (sec a) : by rewrite con_ap_eq_con
+      ... = ((retrfa⁻¹ ⬝ fgfinvsect) ⬝ fgretrfa) ⬝ ap f (sec a)           : by rewrite ap_compose
-          ... = ((retrfa⁻¹ ⬝ fgfinvsect) ⬝ fgretrfa) ⬝ ap f (sec a)           : by rewrite ap_compose
+      ... = (retrfa⁻¹ ⬝ (fgfinvsect ⬝ fgretrfa)) ⬝ ap f (sec a)           : by rewrite con.assoc'
-          ... = (retrfa⁻¹ ⬝ (fgfinvsect ⬝ fgretrfa)) ⬝ ap f (sec a)           : by rewrite con.assoc'
+      ... = retrfa⁻¹ ⬝ ap f (ap g (ap f (sec a)⁻¹) ⬝ ap g (ret (f a))) ⬝ ap f (sec a)   : by rewrite ap_con
-          ... = retrfa⁻¹ ⬝ ap f (ap g (ap f (sec a)⁻¹) ⬝ ap g (ret (f a))) ⬝ ap f (sec a)   : by rewrite ap_con
+      ... = retrfa⁻¹ ⬝ (ap f (ap g (ap f (sec a)⁻¹) ⬝ ap g (ret (f a))) ⬝ ap f (sec a)) : by rewrite con.assoc'
-          ... = retrfa⁻¹ ⬝ (ap f (ap g (ap f (sec a)⁻¹) ⬝ ap g (ret (f a))) ⬝ ap f (sec a)) : by rewrite con.assoc'
+      ... = retrfa⁻¹ ⬝ ap f ((ap g (ap f (sec a)⁻¹) ⬝ ap g (ret (f a))) ⬝ sec a)        : by rewrite -ap_con,
-          ... = retrfa⁻¹ ⬝ ap f ((ap g (ap f (sec a)⁻¹) ⬝ ap g (ret (f a))) ⬝ sec a)        : by rewrite -ap_con,
+  have eq4 : ret (f a) = ap f ((ap g (ap f (sec a)⁻¹) ⬝ ap g (ret (f a))) ⬝ sec a),
-      have eq4 : ret (f a) = ap f ((ap g (ap f (sec a)⁻¹) ⬝ ap g (ret (f a))) ⬝ sec a),
+    from eq_of_idp_eq_inv_con eq3,
-        from eq_of_idp_eq_inv_con eq3,
+  eq4
-      eq4)
 
   definition adjointify [constructor] : is_equiv f :=
-  is_equiv.mk f g ret adjointify_sect' adjointify_adj'
+  is_equiv.mk f g ret adjointify_left_inv' adjointify_adj'
   end
 
   -- Any function pointwise equal to an equivalence is an equivalence as well.
@@ -174,11 +173,12 @@ namespace is_equiv
 
   definition equiv_rect_comp (P : B → Type)
       (df : Π (x : A), P (f x)) (x : A) : equiv_rect f P df (f x) = df x :=
-    calc equiv_rect f P df (f x)
+    calc
-          = transport P (right_inv f (f x)) (df (f⁻¹ (f x)))       : by esimp
+      equiv_rect f P df (f x)
-      ... = transport P (eq.ap f (left_inv f x)) (df (f⁻¹ (f x))) : by rewrite adj
+            = right_inv f (f x) ▸ df (f⁻¹ (f x))   : by esimp
-      ... = transport (P ∘ f) (left_inv f x) (df (f⁻¹ (f x)))     : by rewrite -transport_compose
+        ... = ap f (left_inv f x) ▸ df (f⁻¹ (f x)) : by rewrite -adj
-      ... = df x                                              : by rewrite (apd df (left_inv f x))
+        ... = left_inv f x ▸ df (f⁻¹ (f x))        : by rewrite -transport_compose
+        ... = df x                                 : by rewrite (apd df (left_inv f x))
 
   end
 
@@ -229,12 +229,14 @@ namespace equiv
   variables {A B C : Type}
 
   protected definition MK [reducible] [constructor] (f : A → B) (g : B → A)
-    (right_inv : f ∘ g ~ id) (left_inv : g ∘ f ~ id) : A ≃ B :=
+    (right_inv : Πb, f (g b) = b) (left_inv : Πa, g (f a) = a) : A ≃ B :=
   equiv.mk f (adjointify f g right_inv left_inv)
 
   definition to_inv [reducible] [unfold 3] (f : A ≃ B) : B → A := f⁻¹
-  definition to_right_inv [reducible] [unfold 3] (f : A ≃ B) : f ∘ f⁻¹ ~ id := right_inv f
+  definition to_right_inv [reducible] [unfold 3] (f : A ≃ B) (b : B) : f (f⁻¹ b) = b :=
-  definition to_left_inv [reducible] [unfold 3] (f : A ≃ B) : f⁻¹ ∘ f ~ id := left_inv f
+  right_inv f b
+  definition to_left_inv [reducible] [unfold 3] (f : A ≃ B) (a : A) : f⁻¹ (f a) = a :=
+  left_inv f a
 
   protected definition refl [refl] [constructor] : A ≃ A :=
   equiv.mk id !is_equiv_id

hott/init/funext.hlean

@@ -169,15 +169,14 @@ section
               (λ b c p, eq.rec_on p idp))))
 
   private definition isequiv_tgt_compose {A B : Type}
-      : @is_equiv (A → diagonal B)
+      : is_equiv (compose (pr₂ ∘ pr1) : (A → diagonal B) → (A → B)) :=
-                 (A → B)
+  begin
-                 (compose (pr₂ ∘ pr1)) :=
+    refine @ua_isequiv_postcompose _ _ _ (pr2 ∘ pr1) _,
-    @ua_isequiv_postcompose _ _ _ (pr2 ∘ pr1)
+    fapply adjointify,
-        (is_equiv.adjointify (pr2 ∘ pr1)
+    { intro b, exact ⟨(b, b), idp⟩},
-          (λ x, sigma.mk (x , x) idp) (λx, idp)
+    { intro b, reflexivity},
-          (λ x, sigma.rec_on x
+    { intro a, induction a with q p, induction q, esimp at *, induction p, reflexivity}
-            (λ xy, prod.rec_on xy
+  end
-              (λ b c p, eq.rec_on p idp))))
 
   set_option class.conservative false
   theorem nondep_funext_from_ua {A : Type} {B : Type}

hott/init/path.hlean

@@ -190,7 +190,7 @@ namespace eq
   eq.rec_on p u
 
   -- This idiom makes the operation right associative.
-  notation p `▸` x := transport _ p x
+  infixr `▸` := transport _
 
   definition cast [reducible] [unfold 3] {A B : Type} (p : A = B) (a : A) : B :=
   p ▸ a

hott/init/pathover.hlean

@@ -11,7 +11,7 @@ import .path .equiv
 
 open equiv is_equiv equiv.ops
 
-variables {A A' : Type} {B : A → Type} {C : Πa, B a → Type}
+variables {A A' : Type} {B B' : A → Type} {C : Πa, B a → Type}
           {a a₂ a₃ a₄ : A} {p p' : a = a₂} {p₂ : a₂ = a₃} {p₃ : a₃ = a₄}
           {b b' : B a} {b₂ b₂' : B a₂} {b₃ : B a₃} {b₄ : B a₄}
           {c : C a b} {c₂ : C a₂ b₂}
@@ -240,4 +240,9 @@ namespace eq
   definition change_path (q : p = p') (r : b =[p] b₂) : b =[p'] b₂ :=
   by induction q;exact r
 
+  definition change_path_equiv (f : Π{a}, B a ≃ B' a) (r : b =[p] b₂) : f b =[p] f b₂ :=
+  by induction r;constructor
+
+  definition change_path_equiv' (f : Π{a}, B a ≃ B' a) (r : f b =[p] f b₂) : b =[p] b₂ :=
+  (left_inv f b)⁻¹ ⬝po change_path_equiv (λa, f⁻¹ᵉ) r ⬝op left_inv f b₂
 end eq

hott/types/cubical/cube.hlean

@@ -20,29 +20,50 @@ namespace eq
        {p₁₂₂ : a₀₂₂ = a₂₂₂} {p₂₁₂ : a₂₀₂ = a₂₂₂} {p₂₂₁ : a₂₂₀ = a₂₂₂}
        (s₁₁₀ : square p₀₁₀ p₂₁₀ p₁₀₀ p₁₂₀)
        (s₁₁₂ : square p₀₁₂ p₂₁₂ p₁₀₂ p₁₂₂)
-       (s₁₀₁ : square p₁₀₀ p₁₀₂ p₀₀₁ p₂₀₁)
-       (s₁₂₁ : square p₁₂₀ p₁₂₂ p₀₂₁ p₂₂₁)
        (s₀₁₁ : square p₀₁₀ p₀₁₂ p₀₀₁ p₀₂₁)
-       (s₂₁₁ : square p₂₁₀ p₂₁₂ p₂₀₁ p₂₂₁), Type :=
+       (s₂₁₁ : square p₂₁₀ p₂₁₂ p₂₀₁ p₂₂₁)
+       (s₁₀₁ : square p₁₀₀ p₁₀₂ p₀₀₁ p₂₀₁)
+       (s₁₂₁ : square p₁₂₀ p₁₂₂ p₀₂₁ p₂₂₁), Type :=
   idc : cube ids ids ids ids ids ids
 
-  variables {A : Type} {a₀₀₀ a₂₀₀ a₀₂₀ a₂₂₀ a₀₀₂ a₂₀₂ a₀₂₂ a₂₂₂ : A}
+  variables {A B : Type} {a₀₀₀ a₂₀₀ a₀₂₀ a₂₂₀ a₀₀₂ a₂₀₂ a₀₂₂ a₂₂₂ a a' : A}
             {p₁₀₀ : a₀₀₀ = a₂₀₀} {p₀₁₀ : a₀₀₀ = a₀₂₀} {p₀₀₁ : a₀₀₀ = a₀₀₂}
             {p₁₂₀ : a₀₂₀ = a₂₂₀} {p₂₁₀ : a₂₀₀ = a₂₂₀} {p₂₀₁ : a₂₀₀ = a₂₀₂}
             {p₁₀₂ : a₀₀₂ = a₂₀₂} {p₀₁₂ : a₀₀₂ = a₀₂₂} {p₀₂₁ : a₀₂₀ = a₀₂₂}
             {p₁₂₂ : a₀₂₂ = a₂₂₂} {p₂₁₂ : a₂₀₂ = a₂₂₂} {p₂₂₁ : a₂₂₀ = a₂₂₂}
             {s₁₁₀ : square p₀₁₀ p₂₁₀ p₁₀₀ p₁₂₀}
             {s₁₁₂ : square p₀₁₂ p₂₁₂ p₁₀₂ p₁₂₂}
-            {s₁₀₁ : square p₁₀₀ p₁₀₂ p₀₀₁ p₂₀₁}
-            {s₁₂₁ : square p₁₂₀ p₁₂₂ p₀₂₁ p₂₂₁}
             {s₀₁₁ : square p₀₁₀ p₀₁₂ p₀₀₁ p₀₂₁}
             {s₂₁₁ : square p₂₁₀ p₂₁₂ p₂₀₁ p₂₂₁}
+            {s₁₀₁ : square p₁₀₀ p₁₀₂ p₀₀₁ p₂₀₁}
+            {s₁₂₁ : square p₁₂₀ p₁₂₂ p₀₂₁ p₂₂₁}
+            {b₁ b₂ b₃ b₄ : B}
 
   definition idc    [reducible] [constructor]         := @cube.idc
   definition idcube [reducible] [constructor] (a : A) := @cube.idc A a
   definition rfl1 : cube s₁₁₀ s₁₁₀ vrfl vrfl vrfl vrfl := by induction s₁₁₀; exact idc
-  definition rfl2 : cube hrfl hrfl s₁₀₁ s₁₀₁ hrfl hrfl := by induction s₁₀₁; exact idc
+  definition rfl2 : cube vrfl vrfl s₁₁₀ s₁₁₀ hrfl hrfl := by induction s₁₁₀; exact idc
-  definition rfl3 : cube vrfl vrfl hrfl hrfl s₁₁₀ s₁₁₀ := by induction s₁₁₀; exact idc
+  definition rfl3 : cube hrfl hrfl hrfl hrfl s₁₀₁ s₁₀₁ := by induction s₁₀₁; exact idc
+
+  definition eq_of_cube (c : cube s₁₁₀ s₁₁₂ s₀₁₁ s₂₁₁ s₁₀₁ s₁₂₁) :
+    transpose s₁₀₁⁻¹ᵛ ⬝h s₁₁₀ ⬝h transpose s₁₂₁ =
+      whisker_square (eq_bottom_of_square s₀₁₁) (eq_bottom_of_square s₂₁₁) idp idp s₁₁₂ :=
+  by induction c; reflexivity
+
+  --set_option pp.implicit true
+  definition eq_of_vdeg_cube {s s' : square p₀₁₀ p₂₁₀ p₁₀₀ p₁₂₀}
+    (c : cube s s' vrfl vrfl vrfl vrfl) : s = s' :=
+  begin
+    induction s, exact eq_of_cube c
+  end
+
+  definition square_pathover [unfold 7]
+    {f₁ : A → b₁ = b₂} {f₂ : A → b₃ = b₄} {f₃ : A → b₁ = b₃} {f₄ : A → b₂ = b₄}
+    {p : a = a'}
+    {q : square (f₁ a) (f₂ a) (f₃ a) (f₄ a)} {r : square (f₁ a') (f₂ a') (f₃ a') (f₄ a')}
+    (s : cube q r (vdeg_square (ap f₁ p)) (vdeg_square (ap f₂ p))
+                  (vdeg_square (ap f₃ p)) (vdeg_square (ap f₄ p))) : q =[p] r :=
+  by induction p;apply pathover_idp_of_eq;exact eq_of_vdeg_cube s
 
 
 end eq

hott/types/cubical/cubeover.hlean

@@ -21,11 +21,11 @@ namespace eq
        {p₁₂₂ : a₀₂₂ = a₂₂₂} {p₂₁₂ : a₂₀₂ = a₂₂₂} {p₂₂₁ : a₂₂₀ = a₂₂₂}
        {s₁₁₀ : square p₀₁₀ p₂₁₀ p₁₀₀ p₁₂₀}
        {s₁₁₂ : square p₀₁₂ p₂₁₂ p₁₀₂ p₁₂₂}
-       {s₁₀₁ : square p₁₀₀ p₁₀₂ p₀₀₁ p₂₀₁}
-       {s₁₂₁ : square p₁₂₀ p₁₂₂ p₀₂₁ p₂₂₁}
        {s₀₁₁ : square p₀₁₀ p₀₁₂ p₀₀₁ p₀₂₁}
        {s₂₁₁ : square p₂₁₀ p₂₁₂ p₂₀₁ p₂₂₁}
-       (c : cube s₁₁₀ s₁₁₂ s₁₀₁ s₁₂₁ s₀₁₁ s₂₁₁)
+       {s₁₀₁ : square p₁₀₀ p₁₀₂ p₀₀₁ p₂₀₁}
+       {s₁₂₁ : square p₁₂₀ p₁₂₂ p₀₂₁ p₂₂₁}
+       (c : cube s₁₁₀ s₁₁₂ s₀₁₁ s₂₁₁ s₁₀₁ s₁₂₁)
                        {b₀₂₀ : B a₀₂₀} {b₂₀₀ : B a₂₀₀} {b₂₂₀ : B a₂₂₀}
        {b₀₀₂ : B a₀₀₂} {b₀₂₂ : B a₀₂₂} {b₂₀₂ : B a₂₀₂} {b₂₂₂ : B a₂₂₂}
        {q₁₀₀ : pathover B b₀₀₀ p₁₀₀ b₂₀₀} {q₀₁₀ : pathover B b₀₀₀ p₀₁₀ b₀₂₀}
@@ -36,10 +36,10 @@ namespace eq
        {q₂₁₂ : pathover B b₂₀₂ p₂₁₂ b₂₂₂} {q₂₂₁ : pathover B b₂₂₀ p₂₂₁ b₂₂₂}
        (t₁₁₀ : squareover B s₁₁₀ q₀₁₀ q₂₁₀ q₁₀₀ q₁₂₀)
        (t₁₁₂ : squareover B s₁₁₂ q₀₁₂ q₂₁₂ q₁₀₂ q₁₂₂)
-       (t₁₀₁ : squareover B s₁₀₁ q₁₀₀ q₁₀₂ q₀₀₁ q₂₀₁)
-       (t₁₂₁ : squareover B s₁₂₁ q₁₂₀ q₁₂₂ q₀₂₁ q₂₂₁)
        (t₀₁₁ : squareover B s₀₁₁ q₀₁₀ q₀₁₂ q₀₀₁ q₀₂₁)
-       (t₂₁₁ : squareover B s₂₁₁ q₂₁₀ q₂₁₂ q₂₀₁ q₂₂₁), Type :=
+       (t₂₁₁ : squareover B s₂₁₁ q₂₁₀ q₂₁₂ q₂₀₁ q₂₂₁)
+       (t₁₀₁ : squareover B s₁₀₁ q₁₀₀ q₁₀₂ q₀₀₁ q₂₀₁)
+       (t₁₂₁ : squareover B s₁₂₁ q₁₂₀ q₁₂₂ q₀₂₁ q₂₂₁), Type :=
   idcubeo : cubeover B idc idso idso idso idso idso idso
 
 

hott/types/cubical/square.hlean

@@ -11,9 +11,9 @@ open eq equiv is_equiv
 namespace eq
 
   variables {A B : Type} {a a' a'' a₀₀ a₂₀ a₄₀ a₀₂ a₂₂ a₂₄ a₀₄ a₄₂ a₄₄ a₁ a₂ a₃ a₄ : A}
-            /-a₀₀-/ {p₁₀ : a₀₀ = a₂₀} /-a₂₀-/ {p₃₀ : a₂₀ = a₄₀} /-a₄₀-/
+            /-a₀₀-/ {p₁₀ p₁₀' : a₀₀ = a₂₀} /-a₂₀-/ {p₃₀ : a₂₀ = a₄₀} /-a₄₀-/
-       {p₀₁ : a₀₀ = a₀₂} /-s₁₁-/ {p₂₁ : a₂₀ = a₂₂} /-s₃₁-/ {p₄₁ : a₄₀ = a₄₂}
+       {p₀₁ p₀₁' : a₀₀ = a₀₂} /-s₁₁-/ {p₂₁ p₂₁' : a₂₀ = a₂₂} /-s₃₁-/ {p₄₁ : a₄₀ = a₄₂}
-            /-a₀₂-/ {p₁₂ : a₀₂ = a₂₂} /-a₂₂-/ {p₃₂ : a₂₂ = a₄₂} /-a₄₂-/
+            /-a₀₂-/ {p₁₂ p₁₂' : a₀₂ = a₂₂} /-a₂₂-/ {p₃₂ : a₂₂ = a₄₂} /-a₄₂-/
        {p₀₃ : a₀₂ = a₀₄} /-s₁₃-/ {p₂₃ : a₂₂ = a₂₄} /-s₃₃-/ {p₄₃ : a₄₂ = a₄₄}
             /-a₀₄-/ {p₁₄ : a₀₄ = a₂₄} /-a₂₄-/ {p₃₄ : a₂₄ = a₄₄} /-a₄₄-/
 
@@ -134,6 +134,10 @@ namespace eq
   definition square_of_eq_top (r : p₁₀ = p₀₁ ⬝ p₁₂ ⬝ p₂₁⁻¹) : square p₁₀ p₁₂ p₀₁ p₂₁ :=
   by induction p₂₁; induction p₁₂; esimp at r;induction r;induction p₁₀;exact ids
 
+  definition eq_bottom_of_square [unfold 10] (s₁₁ : square p₁₀ p₁₂ p₀₁ p₂₁)
+    : p₁₂ = p₀₁⁻¹ ⬝ p₁₀ ⬝ p₂₁ :=
+  by induction s₁₁; apply idp
+
   definition square_equiv_eq [constructor] (t : a₀₀ = a₀₂) (b : a₂₀ = a₂₂)
     (l : a₀₀ = a₂₀) (r : a₀₂ = a₂₂) : square t b l r ≃ t ⬝ r = l ⬝ b :=
   begin
@@ -157,7 +161,8 @@ namespace eq
   definition eq_of_vdeg_square [reducible] {p q : a = a'} (s : square p q idp idp) : p = q :=
   to_fun !vdeg_square_equiv' s
 
-  definition top_deg_square (l : a₁ = a₂) (b : a₂ = a₃) (r : a₄ = a₃) : square (l ⬝ b ⬝ r⁻¹) b l r :=
+  definition top_deg_square (l : a₁ = a₂) (b : a₂ = a₃) (r : a₄ = a₃)
+    : square (l ⬝ b ⬝ r⁻¹) b l r :=
   by induction r;induction b;induction l;constructor
 
   /-
@@ -186,7 +191,7 @@ namespace eq
   -- example (p q : a = a') : to_inv (hdeg_square_equiv' p q) = hdeg_square := idp -- this fails
   example (p q : a = a') : to_inv (hdeg_square_equiv p q) = hdeg_square := idp
 
-  definition pathover_eq [unfold 7] {f g : A → B} {p : a = a'} {q : f a = g a} {r : f a' = g a'}
+  definition eq_pathover [unfold 7] {f g : A → B} {p : a = a'} {q : f a = g a} {r : f a' = g a'}
     (s : square q r (ap f p) (ap g p)) : q =[p] r :=
   by induction p;apply pathover_idp_of_eq;exact eq_of_vdeg_square s
 
@@ -197,17 +202,17 @@ namespace eq
 
   /- interaction of equivalences with operations on squares -/
 
-  definition pathover_eq_equiv_square [constructor] {f g : A → B}
+  definition eq_pathover_equiv_square [constructor] {f g : A → B}
     (p : a = a') (q : f a = g a) (r : f a' = g a') : q =[p] r ≃ square q r (ap f p) (ap g p) :=
   equiv.MK square_of_pathover
-           pathover_eq
+           eq_pathover
            begin
-             intro s, induction p, esimp [square_of_pathover,pathover_eq],
+             intro s, induction p, esimp [square_of_pathover,eq_pathover],
              exact ap vdeg_square (to_right_inv !pathover_idp (eq_of_vdeg_square s))
                ⬝ to_left_inv !vdeg_square_equiv s
            end
            begin
-             intro s, induction p, esimp [square_of_pathover,pathover_eq],
+             intro s, induction p, esimp [square_of_pathover,eq_pathover],
              exact ap pathover_idp_of_eq (to_right_inv !vdeg_square_equiv (eq_of_pathover_idp s))
                ⬝ to_left_inv !pathover_idp s
            end
@@ -267,17 +272,17 @@ namespace eq
 
 
   -- the following definition is very slow, maybe it's interesting to see why?
-  -- definition pathover_eq_equiv_square' {f g : A → B}(p : a = a') (q : f a = g a) (r : f a' = g a')
+  -- definition eq_pathover_equiv_square' {f g : A → B}(p : a = a') (q : f a = g a) (r : f a' = g a')
   --   : square q r (ap f p) (ap g p) ≃ q =[p] r :=
-  -- equiv.MK pathover_eq
+  -- equiv.MK eq_pathover
   --          square_of_pathover
   --          (λs, begin
-  --                 induction p, rewrite [↑[square_of_pathover,pathover_eq],
+  --                 induction p, rewrite [↑[square_of_pathover,eq_pathover],
   --                   to_right_inv !vdeg_square_equiv (eq_of_pathover_idp s),
   --                   to_left_inv !pathover_idp s]
   --               end)
   --          (λs, begin
-  --                 induction p, rewrite [↑[square_of_pathover,pathover_eq],▸*,
+  --                 induction p, rewrite [↑[square_of_pathover,eq_pathover],▸*,
   --                   to_right_inv !(@pathover_idp A) (eq_of_vdeg_square s),
   --                   to_left_inv !vdeg_square_equiv s]
   --               end)
@@ -345,6 +350,11 @@ namespace eq
 
   --we can also do the other recursors (tl, tr, bl, br, tbl, tbr, tlr, blr), but let's postpone this until they are needed
 
+  definition whisker_square [unfold 14 15 16 17] (r₁₀ : p₁₀ = p₁₀') (r₁₂ : p₁₂ = p₁₂')
+    (r₀₁ : p₀₁ = p₀₁') (r₂₁ : p₂₁ = p₂₁') (s : square p₁₀ p₁₂ p₀₁ p₂₁)
+      : square p₁₀' p₁₂' p₀₁' p₂₁' :=
+  by induction r₁₀; induction r₁₂; induction r₀₁; induction r₂₁; exact s
+
   /- squares commute with some operations on 2-paths -/
 
   definition square_inv2 {p₁ p₂ p₃ p₄ : a = a'}

hott/types/eq.hlean

@@ -220,7 +220,7 @@ namespace eq
 
   /- Path operations are equivalences -/
 
-  definition is_equiv_eq_inverse (a₁ a₂ : A) : is_equiv (@inverse A a₁ a₂) :=
+  definition is_equiv_eq_inverse (a₁ a₂ : A) : is_equiv (inverse : a₁ = a₂ → a₂ = a₁) :=
   is_equiv.mk inverse inverse inv_inv inv_inv (λp, eq.rec_on p idp)
   local attribute is_equiv_eq_inverse [instance]
 
@@ -253,7 +253,7 @@ namespace eq
   equiv.trans (equiv_eq_closed_left a₃ p) (equiv_eq_closed_right a₂ q)
 
   definition is_equiv_whisker_left (p : a₁ = a₂) (q r : a₂ = a₃)
-  : is_equiv (@whisker_left A a₁ a₂ a₃ p q r) :=
+  : is_equiv (whisker_left p : q = r → p ⬝ q = p ⬝ r) :=
   begin
   fapply adjointify,
     {intro s, apply (!cancel_left s)},
@@ -273,7 +273,7 @@ namespace eq
   equiv.mk _ !is_equiv_whisker_left
 
   definition is_equiv_whisker_right {p q : a₁ = a₂} (r : a₂ = a₃)
-    : is_equiv (λs, @whisker_right A a₁ a₂ a₃ p q s r) :=
+    : is_equiv (λs, whisker_right s r : p = q → p ⬝ r = q ⬝ r) :=
   begin
   fapply adjointify,
     {intro s, apply (!cancel_right s)},

hott/types/equiv.hlean

@@ -9,7 +9,7 @@ Theorems about the types equiv and is_equiv
 
 import .fiber .arrow arity .hprop_trunc
 
-open eq is_trunc sigma sigma.ops pi fiber function equiv
+open eq is_trunc sigma sigma.ops pi fiber function equiv equiv.ops
 
 namespace is_equiv
   variables {A B : Type} (f : A → B) [H : is_equiv f]
@@ -18,14 +18,16 @@ namespace is_equiv
   definition is_contr_fiber_of_is_equiv [instance] (b : B) : is_contr (fiber f b) :=
   is_contr.mk
     (fiber.mk (f⁻¹ b) (right_inv f b))
-    (λz, fiber.rec_on z (λa p, fiber_eq ((ap f⁻¹ p)⁻¹ ⬝ left_inv f a) (calc
+    (λz, fiber.rec_on z (λa p,
-      right_inv f b = (ap (f ∘ f⁻¹) p)⁻¹ ⬝ ((ap (f ∘ f⁻¹) p) ⬝ right_inv f b) : by rewrite inv_con_cancel_left
+      fiber_eq ((ap f⁻¹ p)⁻¹ ⬝ left_inv f a) (calc
-           ... = (ap (f ∘ f⁻¹) p)⁻¹ ⬝ (right_inv f (f a) ⬝ p)       : by rewrite ap_con_eq_con
+        right_inv f b
-           ... = (ap (f ∘ f⁻¹) p)⁻¹ ⬝ (ap f (left_inv f a) ⬝ p)    : by rewrite adj
+          = (ap (f ∘ f⁻¹) p)⁻¹ ⬝ ((ap (f ∘ f⁻¹) p) ⬝ right_inv f b) : by rewrite inv_con_cancel_left
-           ... = (ap (f ∘ f⁻¹) p)⁻¹ ⬝ ap f (left_inv f a) ⬝ p      : by rewrite con.assoc
+      ... = (ap (f ∘ f⁻¹) p)⁻¹ ⬝ (right_inv f (f a) ⬝ p)       : by rewrite ap_con_eq_con
-           ... = (ap f (ap f⁻¹ p))⁻¹ ⬝ ap f (left_inv f a) ⬝ p     : by rewrite ap_compose
+      ... = (ap (f ∘ f⁻¹) p)⁻¹ ⬝ (ap f (left_inv f a) ⬝ p)    : by rewrite adj
-           ... = ap f (ap f⁻¹ p)⁻¹ ⬝ ap f (left_inv f a) ⬝ p       : by rewrite ap_inv
+      ... = (ap (f ∘ f⁻¹) p)⁻¹ ⬝ ap f (left_inv f a) ⬝ p      : by rewrite con.assoc
-           ... = ap f ((ap f⁻¹ p)⁻¹ ⬝ left_inv f a) ⬝ p            : by rewrite ap_con)))
+      ... = (ap f (ap f⁻¹ p))⁻¹ ⬝ ap f (left_inv f a) ⬝ p     : by rewrite ap_compose
+      ... = ap f (ap f⁻¹ p)⁻¹ ⬝ ap f (left_inv f a) ⬝ p       : by rewrite ap_inv
+      ... = ap f ((ap f⁻¹ p)⁻¹ ⬝ left_inv f a) ⬝ p            : by rewrite ap_con)))
 
   definition is_contr_right_inverse : is_contr (Σ(g : B → A), f ∘ g ~ id) :=
   begin
@@ -54,12 +56,12 @@ namespace is_equiv
   equiv.MK (λH, ⟨inv f, right_inv f, left_inv f, adj f⟩)
            (λp, is_equiv.mk f p.1 p.2.1 p.2.2.1 p.2.2.2)
            (λp, begin
-                  cases p with p1 p2,
+                  induction p with p1 p2,
-                  cases p2 with p21 p22,
+                  induction p2 with p21 p22,
-                  cases p22 with p221 p222,
+                  induction p22 with p221 p222,
-                  apply idp
+                  reflexivity
                 end)
-           (λH, is_equiv.rec_on H (λH1 H2 H3 H4, idp))
+           (λH, by induction H; reflexivity)
 
   protected definition sigma_char' : (is_equiv f) ≃
   (Σ(u : Σ(g : B → A), f ∘ g ~ id), Σ(η : u.1 ∘ f ~ id), Π(a : A), u.2 (f a) = ap f (η a)) :=
@@ -116,7 +118,8 @@ namespace equiv
   definition equiv_eq {f f' : A ≃ B} (p : to_fun f = to_fun f') : f = f' :=
   by (cases f; cases f'; apply (equiv_mk_eq p))
 
-  protected definition equiv.sigma_char (A B : Type) : (A ≃ B) ≃ Σ(f : A → B), is_equiv f :=
+  protected definition equiv.sigma_char [constructor]
+    (A B : Type) : (A ≃ B) ≃ Σ(f : A → B), is_equiv f :=
   begin
     fapply equiv.MK,
       {intro F, exact ⟨to_fun F, to_is_equiv F⟩},
@@ -143,4 +146,15 @@ namespace equiv
       {intro p, cases p, cases f with f H, apply ap (ap (equiv.mk f)), apply is_hset.elim}
   end
 
+  definition equiv_pathover {A : Type} {a a' : A} (p : a = a')
+    {B : A → Type} {C : A → Type} (f : B a ≃ C a) (g : B a' ≃ C a')
+    (r : Π(b : B a) (b' : B a') (q : b =[p] b'), f b =[p] g b') : f =[p] g :=
+  begin
+    fapply change_path_equiv',
+    { intro a, apply equiv.sigma_char},
+    { fapply sigma_pathover,
+        esimp, apply arrow_pathover, exact r,
+        apply is_hprop.elimo}
+  end
+
 end equiv

hott/types/hprop_trunc.hlean

@@ -31,8 +31,8 @@ namespace is_trunc
     { intro H x y, apply is_trunc_eq},
     { intro H, cases H, apply idp},
     { intro P, apply eq_of_homotopy, intro a, apply eq_of_homotopy, intro b,
-      esimp [is_trunc_eq], esimp[compose,is_trunc_succ_intro],
+      change is_trunc.mk (to_internal n (a = b)) = P a b,
-      generalize (P a b), intro H, cases H, apply idp},
+      induction (P a b), apply idp},
   end
 
   definition is_hprop_is_trunc [instance] (n : trunc_index) :

hott/types/pi.hlean

@@ -18,11 +18,15 @@ namespace pi
 
   /- Paths -/
 
-  /- Paths [p : f ≈ g] in a function type [Πx:X, P x] are equivalent to functions taking values in path types, [H : Πx:X, f x ≈ g x], or concisely, [H : f ~ g].
+  /-
+    Paths [p : f ≈ g] in a function type [Πx:X, P x] are equivalent to functions taking values
+    in path types, [H : Πx:X, f x ≈ g x], or concisely, [H : f ~ g].
 
-  This equivalence, however, is just the combination of [apd10] and function extensionality [funext], and as such, [path_forall], et seq. are given in axioms.funext and path:  -/
+    This equivalence, however, is just the combination of [apd10] and function extensionality
+    [funext], and as such, [eq_of_homotopy]
 
-  /- Now we show how these things compute. -/
+    Now we show how these things compute.
+  -/
 
   definition apd10_eq_of_homotopy (h : f ~ g) : apd10 (eq_of_homotopy h) ~ h :=
   apd10 (right_inv apd10 h)
@@ -33,17 +37,19 @@ namespace pi
   definition eq_of_homotopy_idp (f : Πa, B a) : eq_of_homotopy (λx : A, refl (f x)) = refl f :=
   !eq_of_homotopy_eta
 
-  /- The identification of the path space of a dependent function space, up to equivalence, is of course just funext. -/
+  /-
+    The identification of the path space of a dependent function space,
+    up to equivalence, is of course just funext.
+  -/
 
   definition eq_equiv_homotopy (f g : Πx, B x) : (f = g) ≃ (f ~ g) :=
-  equiv.mk _ !is_equiv_apd
+  equiv.mk apd10 _
 
-  definition is_equiv_eq_of_homotopy [instance] (f g : Πx, B x)
+  definition is_equiv_eq_of_homotopy (f g : Πx, B x) : is_equiv (@eq_of_homotopy _ _ f g) :=
-      : is_equiv (@eq_of_homotopy _ _ f g) :=
+  _
-  is_equiv_inv apd10
 
   definition homotopy_equiv_eq (f g : Πx, B x) : (f ~ g) ≃ (f = g) :=
-  equiv.mk _ !is_equiv_eq_of_homotopy
+  equiv.mk eq_of_homotopy _
 
 
   /- Transport -/
@@ -56,7 +62,7 @@ namespace pi
   /- A special case of [transport_pi] where the type [B] does not depend on [A],
       and so it is just a fixed type [B]. -/
   definition pi_transport_constant {C : A → A' → Type} (p : a = a') (f : Π(b : A'), C a b) (b : A')
-    : (transport (λa, Π(b : A'), C a b) p f) b = transport (λa, C a b) p (f b) :=
+    : (transport _ p f) b = p ▸ (f b) :=
   eq.rec_on p idp
 
   /- Pathovers -/
@@ -147,10 +153,11 @@ namespace pi
 
   /- The functoriality of [forall] is slightly subtle: it is contravariant in the domain type and covariant in the codomain, but the codomain is dependent on the domain. -/
 
-  definition pi_functor : (Π(a:A), B a) → (Π(a':A'), B' a') := (λg a', f1 a' (g (f0 a')))
+  definition pi_functor [unfold-full] : (Π(a:A), B a) → (Π(a':A'), B' a') := λg a', f1 a' (g (f0 a'))
 
   definition ap_pi_functor {g g' : Π(a:A), B a} (h : g ~ g')
-      : ap (pi_functor f0 f1) (eq_of_homotopy h) = eq_of_homotopy (λa':A', (ap (f1 a') (h (f0 a')))) :=
+    : ap (pi_functor f0 f1) (eq_of_homotopy h)
+      = eq_of_homotopy (λa':A', (ap (f1 a') (h (f0 a')))) :=
   begin
   apply (equiv_rect (@apd10 A B g g')), intro p, clear h,
   cases p,
@@ -161,32 +168,25 @@ namespace pi
 
   /- Equivalences -/
 
-  definition is_equiv_pi_functor [instance]
+  definition is_equiv_pi_functor [instance] [H0 : is_equiv f0]
-    [H0 : is_equiv f0] [H1 : Πa', @is_equiv (B (f0 a')) (B' a') (f1 a')]
+    [H1 : Πa', @is_equiv (B (f0 a')) (B' a') (f1 a')] : is_equiv (pi_functor f0 f1) :=
-      : is_equiv (pi_functor f0 f1) :=
   begin
     apply (adjointify (pi_functor f0 f1) (pi_functor f0⁻¹
           (λ(a : A) (b' : B' (f0⁻¹ a)), transport B (right_inv f0 a) ((f1 (f0⁻¹ a))⁻¹ b')))),
-    intro h, apply eq_of_homotopy,
-    unfold pi_functor, unfold function.compose, unfold function.id,
     begin
-      intro a',
+      intro h, apply eq_of_homotopy, intro a', esimp,
-      apply (tr_rev _ (adj f0 a')),
+      rewrite [adj f0 a',-transport_compose,fn_tr_eq_tr_fn _ f1,right_inv (f1 _)],
-      apply (transport (λx, f1 a' x = h a') (transport_compose B f0 (left_inv f0 a') _)),
-      apply (tr_rev (λx, x = h a') (fn_tr_eq_tr_fn _ f1 _)), unfold function.compose,
-      apply (tr_rev (λx, left_inv f0 a' ▸ x = h a') (right_inv (f1 _) _)), unfold function.id,
       apply apd
     end,
     begin
-      intro h,
+      intro h, apply eq_of_homotopy, intro a, esimp,
-      apply eq_of_homotopy, intro a,
+      rewrite [left_inv (f1 _)],
-      apply (tr_rev (λx, right_inv f0 a ▸ x = h a) (left_inv (f1 _) _)), unfold function.id,
       apply apd
     end
   end
 
-  definition pi_equiv_pi_of_is_equiv [H : is_equiv f0] [H1 : Πa', @is_equiv (B (f0 a')) (B' a') (f1 a')]
+  definition pi_equiv_pi_of_is_equiv [H : is_equiv f0]
-    : (Πa, B a) ≃ (Πa', B' a') :=
+    [H1 : Πa', @is_equiv (B (f0 a')) (B' a') (f1 a')] : (Πa, B a) ≃ (Πa', B' a') :=
   equiv.mk (pi_functor f0 f1) _
 
   definition pi_equiv_pi (f0 : A' ≃ A) (f1 : Πa', (B (to_fun f0 a') ≃ B' a'))

hott/types/pointed.hlean

@@ -67,13 +67,15 @@ namespace pointed
   -- | Iterated_loop_space A 0 := A
   -- | Iterated_loop_space A (n+1) := Iterated_loop_space (Loop_space A) n
 
-  definition Iterated_loop_space [reducible] (n : ℕ) (A : Pointed) : Pointed :=
+  definition Iterated_loop_space [unfold 1] [reducible] (n : ℕ) (A : Pointed) : Pointed :=
   nat.rec_on n (λA, A) (λn IH A, IH (Loop_space A)) A
 
   prefix `Ω`:(max+5) := Loop_space
   notation `Ω[`:95 n:0 `]`:0 A:95 := Iterated_loop_space n A
 
-  definition iterated_loop_space (A : Type) [H : pointed A] (n : ℕ) : Type :=
+  definition refln [constructor] {A : Pointed} {n : ℕ} : Ω[n] A := pt
+
+  definition iterated_loop_space [unfold 3] (A : Type) [H : pointed A] (n : ℕ) : Type :=
   Ω[n] (pointed.mk' A)
 
   open equiv.ops
@@ -202,11 +204,11 @@ namespace pointed
       { esimp, exact !con.left_inv⁻¹}},
   end
 
-  definition apn [constructor] (n : ℕ) (f : map₊ A B) : Ω[n] A →* Ω[n] B :=
+  definition apn [unfold 3] (n : ℕ) (f : map₊ A B) : Ω[n] A →* Ω[n] B :=
   begin
   revert A B f, induction n with n IH,
   { intros A B f, exact f},
-  { intros A B f, esimp [Iterated_loop_space], apply IH (Ω A),
+  { intros A B f, esimp, apply IH (Ω A),
     { esimp, fconstructor,
         intro q, refine !respect_pt⁻¹ ⬝ ap f q ⬝ !respect_pt,
         esimp, apply con.left_inv}}

hott/types/sigma.hlean

@@ -9,10 +9,9 @@ Theorems about sigma-types (dependent sums)
 
 import types.prod
 
-open eq sigma sigma.ops equiv is_equiv
+open eq sigma sigma.ops equiv is_equiv function
 
 namespace sigma
-  local infixr ∘ := function.compose --remove
   variables {A A' : Type} {B : A → Type} {B' : A' → Type} {C : Πa, B a → Type}
             {D : Πa b, C a b → Type}
             {a a' a'' : A} {b b₁ b₂ : B a} {b' : B a'} {b'' : B a''} {u v w : Σa, B a}

hott/types/trunc.hlean

@@ -31,8 +31,8 @@ namespace is_trunc
     fapply equiv.MK,
     { intro A, exact (⟨carrier A, struct A⟩)},
     { intro S, exact (trunctype.mk S.1 S.2)},
-    { intro S, apply (sigma.rec_on S), intro S1 S2, apply idp},
+    { intro S, induction S with S1 S2, reflexivity},
-    { intro A, apply (trunctype.rec_on A), intro A1 A2, apply idp},
+    { intro A, induction A with A1 A2, reflexivity},
   end
 
   definition trunctype_eq_equiv (n : trunc_index) (A B : n-Type) :
@@ -47,7 +47,7 @@ namespace is_trunc
   definition is_trunc_is_embedding_closed (f : A → B) [Hf : is_embedding f] [HB : is_trunc n B]
     (Hn : -1 ≤ n) : is_trunc n A :=
   begin
-    cases n with n,
+    induction n with n,
       {exact !empty.elim Hn},
       {apply is_trunc_succ_intro, intro a a',
          fapply @is_trunc_is_equiv_closed_rev _ _ n (ap f)}
@@ -57,18 +57,18 @@ namespace is_trunc
     (n : trunc_index) [HA : is_trunc n A] : is_trunc n B :=
   begin
     revert A B f Hf HA,
-    eapply (trunc_index.rec_on n),
+    induction n with n IH,
-    { clear n, intro A B f Hf HA, cases Hf with g ε, fapply is_contr.mk,
+    { intro A B f Hf HA, induction Hf with g ε, fapply is_contr.mk,
       { exact f (center A)},
       { intro b, apply concat,
         { apply (ap f), exact (center_eq (g b))},
         { apply ε}}},
-    { clear n, intro n IH A B f Hf HA, cases Hf with g ε,
+    { intro A B f Hf HA, induction Hf with g ε,
       apply is_trunc_succ_intro, intro b b',
       fapply (IH (g b = g b')),
       { intro q, exact ((ε b)⁻¹ ⬝ ap f q ⬝ ε b')},
       { apply (is_retraction.mk (ap g)),
-        { intro p, cases p, {rewrite [↑ap, con.left_inv]}}},
+        { intro p, induction p, {rewrite [↑ap, con.left_inv]}}},
       { apply is_trunc_eq}}
   end
 
@@ -82,7 +82,7 @@ namespace is_trunc
       {apply equiv.symm, apply trunctype_eq_equiv},
     fapply is_trunc_equiv_closed,
       {apply equiv.symm, apply eq_equiv_equiv},
-    cases n,
+    induction n,
       {apply @is_contr_of_inhabited_hprop,
         {apply is_trunc_is_embedding_closed,
           {apply is_embedding_to_fun} ,
@@ -143,7 +143,7 @@ namespace is_trunc
   begin
     apply is_trunc_succ_intro, intros a a',
     apply is_trunc_of_imp_is_trunc_of_leq Hn, intro p,
-    cases p, apply Hp
+    induction p, apply Hp
   end
 
   definition is_trunc_succ_iff_is_trunc_loop (A : Type) (Hn : -1 ≤ n) :
@@ -176,7 +176,7 @@ namespace is_trunc
   definition is_trunc_iff_is_contr_loop (n : ℕ) (A : Type)
     : is_trunc (n.-2.+1) A ↔ (Π(a : A), is_contr (Ω[n](pointed.Mk a))) :=
   begin
-    cases n with n,
+    induction n with n,
     { esimp [sub_two,Iterated_loop_space], apply iff.intro,
         intro H a, exact is_contr_of_inhabited_hprop a,
         intro H, apply is_hprop_of_imp_is_contr, exact H},
@@ -193,7 +193,7 @@ namespace trunc
 
   protected definition encode (n : trunc_index) (aa aa' : trunc n.+1 A) : aa = aa' → trunc.code n aa aa' :=
   begin
-    intro p, cases p, apply (trunc.rec_on aa),
+    intro p, induction p, apply (trunc.rec_on aa),
     intro a, esimp [trunc.code,trunc.rec_on], exact (tr idp)
   end
 
@@ -212,8 +212,10 @@ namespace trunc
     { apply trunc.decode},
     { eapply (trunc.rec_on aa'), eapply (trunc.rec_on aa),
       intro a a' x, esimp [trunc.code, trunc.rec_on] at x,
-      apply (trunc.rec_on x), intro p, cases p, exact idp},
+      refine (@trunc.rec_on n _ _ x _ _),
-    { intro p, cases p, apply (trunc.rec_on aa), intro a, exact idp},
+        intro x, apply is_trunc_eq,
+        intro p, induction p, reflexivity},
+    { intro p, induction p, apply (trunc.rec_on aa), intro a, exact idp},
   end
 
   definition tr_eq_tr_equiv (n : trunc_index) (a a' : A)
@@ -226,7 +228,7 @@ namespace trunc
     revert A m H, eapply (trunc_index.rec_on n),
     { clear n, intro A m H, apply is_contr_equiv_closed,
       { apply equiv_trunc, apply (@is_trunc_of_leq _ -2), exact unit.star} },
-    { clear n, intro n IH A m H, cases m with m,
+    { clear n, intro n IH A m H, induction m with m,
       { apply (@is_trunc_of_leq _ -2), exact unit.star},
       { apply is_trunc_succ_intro, intro aa aa',
         apply (@trunc.rec_on _ _ _ aa  (λy, !is_trunc_succ_of_is_hprop)),

tests/lean/hott/433.hlean

@@ -112,10 +112,9 @@ namespace pi
   rewrite {f1 a' _}(fn_tr_eq_tr_fn _ f1 _),
   rewrite (right_inv (f1 _) _),
   apply apd,
-  intro h, beta,
+  intro h,
   apply eq_of_homotopy, intro a, esimp,
   apply (transport_V (λx, right_inv f0 a ▸ x = h a) (left_inv (f1 _) _)),
-  esimp [function.id],
   apply apd
   end
 

tests/lean/hott/unfold_test.hlean

@@ -26,7 +26,7 @@ section
     apply sorry,
     apply sorry,
     {
-      rewrite [↑e_closure.elim, ↑ap_e_closure_elim_h, ap_con (ap h)],
+      rewrite [▸*, ap_con (ap h)],
       refine (transpose !ap_compose_inv)⁻¹ᵛ ⬝h _,
       rewrite [con_inv,inv_inv,-inv2_inv],
       exact !ap_inv2 ⬝v square_inv2 v_0