feat(categories): prove introduction rule for equivalences

hott/algebra/category/adjoint.hlean

@@ -27,9 +27,11 @@ namespace category
     (H : Π(c : C), ε (F c) ∘ F (η c) = ID (F c))
     (K : Π(d : D), G (ε d) ∘ η (G d) = ID (G d))
 
-  abbreviation right_adjoint := @is_left_adjoint.G
+  abbreviation right_adjoint  [unfold 4] := @is_left_adjoint.G
-  abbreviation unit          := @is_left_adjoint.η
+  abbreviation unit           [unfold 4] := @is_left_adjoint.η
-  abbreviation counit        := @is_left_adjoint.ε
+  abbreviation counit         [unfold 4] := @is_left_adjoint.ε
+  abbreviation counit_unit_eq [unfold 4] := @is_left_adjoint.H
+  abbreviation unit_counit_eq [unfold 4] := @is_left_adjoint.K
 
   structure is_equivalence [class] (F : C ⇒ D) extends is_left_adjoint F :=
     mk' ::
@@ -38,7 +40,7 @@ namespace category
 
   abbreviation inverse := @is_equivalence.G
   postfix ⁻¹ := inverse
-  --a second notation for the inverse, which is not overloaded
+  --a second notation for the inverse, which is not overloaded (there is no unicode superscript F)
   postfix [parsing_only] `⁻¹F`:std.prec.max_plus := inverse
 
   --TODO: review and change
@@ -59,8 +61,8 @@ namespace category
     (struct : is_isomorphism to_functor)
   --   infix `⊣`:55 := adjoint
 
-  infix ` ⋍ `:25 := equivalence -- \backsimeq or \equiv
+  infix ` ≃c `:25 := equivalence
-  infix ` ≌ `:25 := isomorphism -- \backcong or \iso
+  infix ` ≅c `:25 := isomorphism
 
   definition is_equiv_of_fully_faithful [instance] [reducible] (F : C ⇒ D) [H : fully_faithful F]
     (c c' : C) : is_equiv (@(to_fun_hom F) c c') :=
@@ -235,128 +237,85 @@ namespace category
   section
     parameters {C D : Precategory} {F : C ⇒ D} {G : D ⇒ C} (η : G ∘f F ≅ 1) (ε : F ∘f G ≅ 1)
 
-      -- variables (η : Πc, G (F c) ≅ c) (ε : Πd, F (G d) ≅ d)
+     -- variables (η : Πc, G (F c) ≅ c) (ε : Πd, F (G d) ≅ d)
-      -- (pη : Π(c c' : C) (f : hom c c'), f ∘ to_hom (η c) = to_hom (η c') ∘ G (F f))
+     -- (pη : Π(c c' : C) (f : hom c c'), f ∘ to_hom (η c) = to_hom (η c') ∘ G (F f))
-      -- (pε : Π⦃d d' : D⦄ (f : hom d d'), f ∘ to_hom (ε d) = to_hom (ε d') ∘ F (G f))
+     -- (pε : Π⦃d d' : D⦄ (f : hom d d'), f ∘ to_hom (ε d) = to_hom (ε d') ∘ F (G f))
 
-     private definition ηn : 1 ⟹ G ∘f F := to_inv η
+    private definition ηn : 1 ⟹ G ∘f F := to_inv η
-     private definition εn : F ∘f G ⟹ 1 := to_hom ε
+    private definition εn : F ∘f G ⟹ 1 := to_hom ε
 
-     private definition ηi (c : C) : G (F c) ≅ c := componentwise_iso η c
+    private definition ηi (c : C) : G (F c) ≅ c := componentwise_iso η c
-     private definition εi (d : D) : F (G d) ≅ d := componentwise_iso ε d
+    private definition εi (d : D) : F (G d) ≅ d := componentwise_iso ε d
 
-     private definition ηi' (c : C) : G (F c) ≅ c :=
+    private definition ηi' (c : C) : G (F c) ≅ c :=
-     to_fun_iso G (to_fun_iso F (ηi c)⁻¹ⁱ) ⬝i to_fun_iso G (εi (F c)) ⬝i ηi c
+    to_fun_iso G (to_fun_iso F (ηi c)⁻¹ⁱ) ⬝i to_fun_iso G (εi (F c)) ⬝i ηi c
-exit
-  set_option pp.implicit true
-     private theorem adj_η_natural {c c' : C} (f : hom c c')
-       : G (F f) ∘ to_inv (ηi' c) = to_inv (ηi c') ∘ f :=
-     let ηi'_nat : G ∘f F ⟹ 1 :=
-         /-    1  ⇐ G ∘f F               :-/ to_hom η
-      ∘n /-   ... ⇐ (G ∘f 1) ∘f F        :-/ hom_of_eq !functor.id_right ∘nf F
-      ∘n /-   ... ⇐ (G ∘f (F ∘f G)) ∘f F :-/ (G ∘fn εn) ∘nf F
-      ∘n /-   ... ⇐ ((G ∘f F) ∘f G) ∘f F :-/ hom_of_eq !functor.assoc⁻¹ ∘nf F
-      ∘n /-   ... ⇐ (G ∘f F) ∘f (G ∘f F) :-/ hom_of_eq !functor.assoc
-      ∘n /-   ... ⇐ (G ∘f F) ∘f 1        :-/ (G ∘f F) ∘fn ηn
-      ∘n /-   ... ⇐ G ∘f F               :-/ hom_of_eq !functor.id_right⁻¹
-       in
-     have ηi'_nat ~ ηi', begin intro c, fold [precategory_functor C C]
-       /-rewrite [+natural_map_hom_of_eq],-/ end,
-     _
 
-     private theorem adjointify_adjH (c : C) :
+    local attribute ηn εn ηi εi ηi' [reducible]
-       to_hom (ε (F c)) ∘ F (to_hom (adj_η η ε c)⁻¹ⁱ) = id  :=
-     begin
-       exact sorry
-     end
 
-     private theorem adjointify_adjK (d : D) :
+    private theorem adj_η_natural {c c' : C} (f : hom c c')
-       G (to_hom (ε d)) ∘ to_hom (adj_η η ε (G d))⁻¹ⁱ = id :=
+      : G (F f) ∘ to_inv (ηi' c) = to_inv (ηi' c') ∘ f :=
-     begin
+    let ηi'_nat : G ∘f F ⟹ 1 :=
-       exact sorry
+    calc
-     end
+      G ∘f F ⟹ (G ∘f F) ∘f 1        : id_right_natural_rev (G ∘f F)
-
+         ... ⟹ (G ∘f F) ∘f (G ∘f F) : (G ∘f F) ∘fn ηn
-    attribute functor.id [reducible]
+         ... ⟹ ((G ∘f F) ∘f G) ∘f F : assoc_natural (G ∘f F) G F
-    variables (F G)
+         ... ⟹ (G ∘f (F ∘f G)) ∘f F : assoc_natural_rev G F G ∘nf F
-    definition is_equivalence.mk : is_equivalence F :=
+         ... ⟹ (G ∘f 1) ∘f F        : (G ∘fn εn) ∘nf F
+         ... ⟹ G ∘f F               : id_right_natural G ∘nf F
+         ... ⟹ 1                    : to_hom η
+    in
     begin
-      fapply is_equivalence.mk',
+     refine is_natural_inverse' (G ∘f F) functor.id ηi' ηi'_nat _ f,
-      { exact G},
+     intro c, esimp, rewrite [+id_left,id_right]
-      { fapply nat_trans.mk,
-        { intro c, exact to_inv (adj_η η ε c)},
-        { intro c c' f, exact adj_η_natural η ε pη pε f}},
-      { fapply nat_trans.mk,
-        { exact λd, to_hom (ε d)},
-        { exact pε}},
-      { exact adjointify_adjH η ε pη pε},
-      { exact adjointify_adjK η ε pη pε},
-      { exact @(is_iso_nat_trans _) (λc, !is_iso_inverse)},
-      { apply is_iso_nat_trans},
     end
 
-  end
+    private theorem adjointify_adjH (c : C) :
+      to_hom (εi (F c)) ∘ F (to_hom (ηi' c))⁻¹ = id :=
+    begin
+      rewrite [respect_inv], apply comp_inverse_eq_of_eq_comp,
+      rewrite [id_left,↑ηi',+respect_comp,+respect_inv',assoc], apply eq_comp_inverse_of_comp_eq,
+      rewrite [↑εi,-naturality_iso_id ε (F c)],
+      symmetry, exact naturality εn (F (to_hom (ηi c)))
+    end
 
-  definition is_equivalence.mk2 (η : G ∘f F ≅ 1) (ε : F ∘f G ≅ 1) : is_equivalence F :=
+    private theorem adjointify_adjK (d : D) :
-  is_equivalence.mk F G
+      G (to_hom (εi d)) ∘ to_hom (ηi' (G d))⁻¹ⁱ = id :=
-    (componentwise_iso η) (componentwise_iso ε)
+    begin
-    begin intro c c' f, esimp, apply naturality (to_hom η) f end
+      apply comp_inverse_eq_of_eq_comp,
-    begin intro c c' f, esimp, apply naturality (to_hom ε) f end
+      rewrite [id_left,↑ηi',+respect_inv',assoc], apply eq_comp_inverse_of_comp_eq,
+      rewrite [↑ηi,-naturality_iso_id η (G d),↑εi,naturality_iso_id ε d],
+      exact naturality (to_hom η) (G (to_hom (εi d))),
+    end
 
-exit
+    parameters (F G)
-
-  section
-    variables (η : G ∘f F ≅ 1) (ε : F ∘f G ≅ 1) -- we need some kind of naturality
     include η ε
-
-     -- private definition adj_η : G ∘f F ≅ functor.id :=
-     -- change_inv
-     -- ( calc
-     --     G ∘f F ≅ (G ∘f F) ∘f 1        : iso_of_eq !functor.id_right
-     --        ... ≅ (G ∘f F) ∘f (G ∘f F) : _
-     --        ... ≅ G ∘f (F ∘f (G ∘f F)) : _
-     --        ... ≅ G ∘f ((F ∘f G) ∘f F) : _
-     --        ... ≅ G ∘f (1 ∘f F)        : _
-     --        ... ≅ G ∘f F               : _
-     --        ... ≅ 1                    : η)
-     --   _
-     --   _ --change_natural_map _ _
-     --sorry --to_fun_iso G (to_fun_iso F (η c)⁻¹ⁱ) ⬝i to_fun_iso G (ε (F c)) ⬝i η c
-     open iso
-
-     -- definition nat_map_of_iso [reducible] {C D : Precategory} {F G : C ⇒ D} (η : F ≅ G) (c : C)
-     --   : F c ⟶ G c :=
-     -- natural_map (to_hom η) c
-
-     private theorem adjointify_adjH (c : C) :
-       natural_map (to_hom ε) (F c) ∘ F (natural_map (to_inv (adj_η η ε)) c) = id  :=
-     begin
-       exact sorry
-     end
-
-    -- (H : Π(c : C), ε (F c) ∘ F (η c) = ID (F c))
-    -- (K : Π(d : D), G (ε d) ∘ η (G d) = ID (G d))
-
-     private theorem adjointify_adjK (d : D) :
-       G (natural_map (to_hom ε) d) ∘ natural_map (to_inv (adj_η η ε)) (G d) = id :=
-     begin
-       exact sorry
-     end
-
-    variables (F G)
     definition is_equivalence.mk : is_equivalence F :=
     begin
       fapply is_equivalence.mk',
       { exact G},
-      { exact to_inv (adj_η η ε)},
+      { fapply nat_trans.mk,
-      { exact to_hom ε},
+        { intro c, exact to_inv (ηi' c)},
-      { exact adjointify_adjH η ε},
+        { intro c c' f, exact adj_η_natural f}},
-      { exact adjointify_adjK η ε},
+      { exact εn},
-      { unfold to_inv, apply is_iso_inverse},
+      { exact adjointify_adjH},
-      { apply iso.struct},
+      { exact adjointify_adjK},
+      { exact @(is_iso_nat_trans _) (λc, !is_iso_inverse)},
+      { unfold εn, apply iso.struct, },
     end
 
+    definition equivalence.MK : C ≃c D :=
+    equivalence.mk F is_equivalence.mk
+  end
+
+  variables {C D : Precategory} {F : C ⇒ D} {G : D ⇒ C}
+
+  --TODO: add variants
+  definition unit_eq_counit_inv (F : C ⇒ D) [H : is_equivalence F] (c : C) :
+    to_fun_hom F (natural_map (unit F) c) =
+    @(is_iso.inverse (counit F (F c))) (@(componentwise_is_iso (counit F)) !is_iso_counit (F c)) :=
+  begin
+    apply eq_inverse_of_comp_eq_id, apply counit_unit_eq
   end
-/-
 
   definition fully_faithful_of_is_equivalence (F : C ⇒ D) [H : is_equivalence F]
     : fully_faithful F :=
@@ -367,10 +326,77 @@ exit
     { intro g, rewrite [+respect_comp,▸*],
       krewrite [natural_map_inverse], xrewrite [respect_inv'],
       apply inverse_comp_eq_of_eq_comp,
-      exact sorry /-this is basically the naturality of the counit-/ },
+      let H := @(naturality (F ∘fn (unit F))),
+      rewrite [+unit_eq_counit_inv], exact sorry},
+    /-this is basically the naturality of the counit-/
     { exact sorry},
   end
 
+  definition is_isomorphism.mk {F : C ⇒ D} (G : D ⇒ C) (p : G ∘f F = 1) (q : F ∘f G = 1)
+    : is_isomorphism F :=
+  begin
+    constructor,
+    { apply fully_faithful_of_is_equivalence, fapply is_equivalence.mk,
+      { exact G},
+      { apply iso_of_eq p},
+      { apply iso_of_eq q}},
+    { fapply adjointify,
+      { exact G},
+      { exact ap010 to_fun_ob q},
+      { exact ap010 to_fun_ob p}}
+  end
+
+  definition is_equiv_of_is_isomorphism (F : C ⇒ D) [H : is_isomorphism F]
+    : is_equiv (to_fun_ob F) :=
+  pr2 H
+
+  definition is_fully_faithful_of_is_isomorphism (F : C ⇒ D) [H : is_isomorphism F]
+    : fully_faithful F :=
+  pr1 H
+
+  local attribute is_fully_faithful_of_is_isomorphism is_equiv_of_is_isomorphism [instance]
+
+  definition strict_inverse [constructor] (F : C ⇒ D) [H : is_isomorphism F] : D ⇒ C :=
+  begin
+    fapply functor.mk,
+    { intro d, exact (to_fun_ob F)⁻¹ᶠ d},
+    { intro d d' g, exact (to_fun_hom F)⁻¹ᶠ (inv_of_eq !right_inv ∘ g ∘ hom_of_eq !right_inv)},
+    { intro d, apply inv_eq_of_eq, rewrite [respect_id,id_left], apply left_inverse},
+    { intro d₁ d₂ d₃ g₂ g₁, apply inv_eq_of_eq, rewrite [respect_comp F,+right_inv (to_fun_hom F)],
+      rewrite [+assoc], esimp, /-apply ap (λx, _ ∘ x), FAILS-/ refine ap (λx, (x ∘ _) ∘ _) _,
+      refine !id_right⁻¹ ⬝ _, rewrite [▸*,-+assoc], refine ap (λx, _ ∘ _ ∘ x) _,
+      exact !right_inverse⁻¹},
+  end
+
+  definition strict_right_inverse (F : C ⇒ D) [H : is_isomorphism F] : F ∘f strict_inverse F = 1 :=
+  begin
+    fapply functor_eq,
+    { intro d, esimp, apply right_inv},
+    { intro d d' g,
+      rewrite [▸*, right_inv (to_fun_hom F), +assoc],
+      rewrite [↑[hom_of_eq,inv_of_eq,iso.to_inv], right_inverse],
+      rewrite [id_left], apply comp_inverse_cancel_right},
+  end
+
+  definition strict_left_inverse (F : C ⇒ D) [H : is_isomorphism F] : strict_inverse F ∘f F = 1 :=
+  begin
+    fapply functor_eq,
+    { intro d, esimp, apply left_inv},
+    { intro d d' g, esimp, apply comp_eq_of_eq_inverse_comp, apply comp_inverse_eq_of_eq_comp,
+      apply inv_eq_of_eq, rewrite [+respect_comp,-assoc], apply ap011 (λx y, x ∘ F g ∘ y),
+      { rewrite [adj], rewrite [▸*,respect_inv_of_eq F]},
+      { rewrite [adj,▸*,respect_hom_of_eq F]}},
+  end
+
+  definition is_equivalence_of_is_isomorphism [instance] (F : C ⇒ D) [H : is_isomorphism F]
+    : is_equivalence F :=
+  begin
+    fapply is_equivalence.mk,
+    { apply strict_inverse F},
+    { apply iso_of_eq !strict_left_inverse},
+    { apply iso_of_eq !strict_right_inverse},
+  end
+
   definition fully_faithful_equiv (F : C ⇒ D) : fully_faithful F ≃ (faithful F × full F) :=
   sorry
 
@@ -400,23 +426,20 @@ exit
     ≃ ∃(G : D ⇒ C), 1 = G ∘f F × F ∘f G = 1 :=
   sorry
 
-  definition is_equivalence_of_isomorphism (H : is_isomorphism F) : is_equivalence F :=
-  sorry
-
   definition is_isomorphism_of_is_equivalence {C D : Category} {F : C ⇒ D} (H : is_equivalence F)
     : is_isomorphism F :=
   sorry
 
-  definition isomorphism_of_eq {C D : Precategory} (p : C = D) : C ≌ D :=
+  definition isomorphism_of_eq {C D : Precategory} (p : C = D) : C ≅c D :=
   sorry
 
   definition is_equiv_isomorphism_of_eq (C D : Precategory) : is_equiv (@isomorphism_of_eq C D) :=
   sorry
 
-  definition equivalence_of_eq {C D : Precategory} (p : C = D) : C ⋍ D :=
+  definition equivalence_of_eq {C D : Precategory} (p : C = D) : C ≃c D :=
   sorry
 
   definition is_equiv_equivalence_of_eq (C D : Category) : is_equiv (@equivalence_of_eq C D) :=
   sorry
--/
+
 end category

hott/algebra/category/category.hlean

@@ -14,8 +14,9 @@ open iso is_equiv equiv eq is_trunc
 -/
 namespace category
   /-
-    TODO: restructure this. is_univalent should probably be a class with as argument
+    TODO: restructure this. Should is_univalent be a class with as argument
-    (C : Precategory)
+    (C : Precategory). Or is that problematic if we want to apply this to cases where e.g.
+    a b are functors, and we need to synthesize ? : precategory (functor C D).
   -/
   definition is_univalent [class] {ob : Type} (C : precategory ob) :=
   Π(a b : ob), is_equiv (iso_of_eq : a = b → a ≅ b)

hott/algebra/category/colimits.hlean

@@ -168,7 +168,8 @@ namespace category
   definition coproduct_object : D :=
   colimit_object (c2_functor D d d')
 
-  infixr + := coproduct_object
+  infixr `+l`:27 := coproduct_object
+  local infixr + := coproduct_object
 
   definition inl : d ⟶ d + d' :=
   colimit_morphism (c2_functor D d d') ff
@@ -317,4 +318,8 @@ namespace category
     : has_limits_of_shape D I :=
   by induction I with I Is; induction Is; exact H
 
+  namespace ops
+  infixr + := coproduct_object
+  end ops
+
 end category

hott/algebra/category/constructions/functor.hlean

@@ -65,13 +65,27 @@ namespace functor
   definition functor_iso [constructor] : F ≅ G :=
   @(iso.mk η) !is_iso_nat_trans
 
+  omit iso
+  variables (F G)
+
+  definition is_natural_inverse (η : Πc, F c ≅ G c)
+    (nat : Π⦃a b : C⦄ (f : hom a b), G f ∘ to_hom (η a) = to_hom (η b) ∘ F f)
+    {a b : C} (f : hom a b) : F f ∘ to_inv (η a) = to_inv (η b) ∘ G f :=
+  let η' : F ⟹ G := nat_trans.mk (λc, to_hom (η c)) @nat in
+  naturality (nat_trans_inverse η') f
+
+  definition is_natural_inverse' (η₁ : Πc, F c ≅ G c) (η₂ : F ⟹ G) (p : η₁ ~ η₂)
+    {a b : C} (f : hom a b) : F f ∘ to_inv (η₁ a) = to_inv (η₁ b) ∘ G f :=
+  is_natural_inverse F G η₁ abstract λa b g, (p a)⁻¹ ▸ (p b)⁻¹ ▸ naturality η₂ g end f
+
   end
 
+
   section
   /- and conversely, if a natural transformation is an iso, it is componentwise an iso -/
   variables {A B C D : Precategory} {F G : C ⇒ D} (η : hom F G) [isoη : is_iso η] (c : C)
   include isoη
-  definition componentwise_is_iso [instance] [constructor] : is_iso (η c) :=
+  definition componentwise_is_iso [constructor] : is_iso (η c) :=
   @is_iso.mk _ _ _ _ _ (natural_map η⁻¹ c) (ap010 natural_map ( left_inverse η) c)
                                            (ap010 natural_map (right_inverse η) c)
 
@@ -105,6 +119,11 @@ namespace functor
     : componentwise_iso (iso_of_eq p) c = iso_of_eq (ap010 to_fun_ob p c) :=
   eq.rec_on p !componentwise_iso_id
 
+  theorem naturality_iso_id {F : C ⇒ C} (η : F ≅ 1) (c : C)
+    : componentwise_iso η (F c) = F (componentwise_iso η c) :=
+  comp.cancel_left (to_hom (componentwise_iso η c))
+    ((naturality (to_hom η)) (to_hom (componentwise_iso η c)))
+
   definition natural_map_hom_of_eq (p : F = G) (c : C)
     : natural_map (hom_of_eq p) c = hom_of_eq (ap010 to_fun_ob p c) :=
   eq.rec_on p idp

hott/algebra/category/functor.hlean

@@ -124,6 +124,18 @@ namespace functor
     : to_fun_iso F (f ⬝i g) = to_fun_iso F f ⬝i to_fun_iso F g :=
   iso_eq !respect_comp
 
+  definition respect_iso_of_eq (F : C ⇒ D) {a b : C} (p : a = b) :
+    to_fun_iso F (iso_of_eq p) = iso_of_eq (ap F p) :=
+  by induction p; apply respect_refl
+
+  theorem respect_hom_of_eq (F : C ⇒ D) {a b : C} (p : a = b) :
+    F (hom_of_eq p) = hom_of_eq (ap F p) :=
+  by induction p; apply respect_id
+
+  definition respect_inv_of_eq (F : C ⇒ D) {a b : C} (p : a = b) :
+    F (inv_of_eq p) = inv_of_eq (ap F p) :=
+  by induction p; apply respect_id
+
   protected definition assoc (H : C ⇒ D) (G : B ⇒ C) (F : A ⇒ B) :
       H ∘f (G ∘f F) = (H ∘f G) ∘f F :=
   !functor_mk_eq_constant (λa b f, idp)

hott/algebra/category/groupoid.hlean

@@ -16,7 +16,7 @@ namespace category
   mk' :: (all_iso : Π ⦃a b : ob⦄ (f : hom a b), @is_iso ob parent a b f)
 
   abbreviation all_iso := @groupoid.all_iso
-  attribute groupoid.all_iso [instance] [priority 100000]
+  attribute groupoid.all_iso [instance] [priority 3000]
 
   definition groupoid.mk [reducible] {ob : Type} (C : precategory ob)
     (H : Π (a b : ob) (f : a ⟶ b), is_iso f) : groupoid ob :=

hott/algebra/category/iso.hlean

@@ -132,7 +132,7 @@ structure iso {ob : Type} [C : precategory ob] (a b : ob) :=
   [struct : is_iso to_hom]
 
   infix ` ≅ `:50 := iso
-  attribute iso.struct [instance] [priority 4000]
+  attribute iso.struct [instance] [priority 2000]
 
 namespace iso
   variables {ob : Type} [C : precategory ob]
@@ -146,7 +146,7 @@ namespace iso
   @(mk f) (is_iso.mk H1 H2)
 
   variable {C}
-  definition to_inv [unfold 5] (f : a ≅ b) : b ⟶ a := (to_hom f)⁻¹
+  definition to_inv [reducible] [unfold 5] (f : a ≅ b) : b ⟶ a := (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 :=
@@ -300,72 +300,79 @@ namespace iso
                            (r : c ⟶ d) (q : b ⟶ c) (p : a ⟶ b)
                            (g : d ⟶ c)
   variable [Hq : is_iso q] include Hq
-  definition comp.right_inverse : q ∘ q⁻¹ = id := !right_inverse
+  theorem comp.right_inverse : q ∘ q⁻¹ = id := !right_inverse
-  definition comp.left_inverse : q⁻¹ ∘ q = id := !left_inverse
+  theorem comp.left_inverse : q⁻¹ ∘ q = id := !left_inverse
-  definition inverse_comp_cancel_left : q⁻¹ ∘ (q ∘ p) = p :=
+
+  theorem inverse_comp_cancel_left : q⁻¹ ∘ (q ∘ p) = p :=
    by rewrite [assoc, left_inverse, id_left]
-  definition comp_inverse_cancel_left : q ∘ (q⁻¹ ∘ g) = g :=
+  theorem comp_inverse_cancel_left : q ∘ (q⁻¹ ∘ g) = g :=
    by rewrite [assoc, right_inverse, id_left]
-  definition comp_inverse_cancel_right : (r ∘ q) ∘ q⁻¹ = r :=
+  theorem comp_inverse_cancel_right : (r ∘ q) ∘ q⁻¹ = r :=
   by rewrite [-assoc, right_inverse, id_right]
-  definition inverse_comp_cancel_right : (f ∘ q⁻¹) ∘ q = f :=
+  theorem inverse_comp_cancel_right : (f ∘ q⁻¹) ∘ q = f :=
   by rewrite [-assoc, left_inverse, id_right]
 
-  definition comp_inverse [Hp : is_iso p] [Hpq : is_iso (q ∘ p)] : (q ∘ p)⁻¹ʰ = p⁻¹ʰ ∘ q⁻¹ʰ :=
+  theorem comp_inverse [Hp : is_iso p] [Hpq : is_iso (q ∘ p)] : (q ∘ p)⁻¹ʰ = p⁻¹ʰ ∘ q⁻¹ʰ :=
   inverse_eq_left
     (show (p⁻¹ʰ ∘ q⁻¹ʰ) ∘ q ∘ p = id, from
      by rewrite [-assoc, inverse_comp_cancel_left, left_inverse])
 
-  definition inverse_comp_inverse_left [H' : is_iso g] : (q⁻¹ ∘ g)⁻¹ = g⁻¹ ∘ q :=
+  theorem inverse_comp_inverse_left [H' : is_iso g] : (q⁻¹ ∘ g)⁻¹ = g⁻¹ ∘ q :=
   inverse_involutive q ▸ comp_inverse q⁻¹ g
 
-  definition inverse_comp_inverse_right [H' : is_iso f] : (q ∘ f⁻¹)⁻¹ = f ∘ q⁻¹ :=
+  theorem inverse_comp_inverse_right [H' : is_iso f] : (q ∘ f⁻¹)⁻¹ = f ∘ q⁻¹ :=
   inverse_involutive f ▸ comp_inverse q f⁻¹
 
-  definition inverse_comp_inverse_inverse [H' : is_iso r] : (q⁻¹ ∘ r⁻¹)⁻¹ = r ∘ q :=
+  theorem inverse_comp_inverse_inverse [H' : is_iso r] : (q⁻¹ ∘ r⁻¹)⁻¹ = r ∘ q :=
   inverse_involutive r ▸ inverse_comp_inverse_left q r⁻¹
   end
 
   section
   variables {ob : Type} {C : precategory ob} include C
   variables {d           c           b           a : ob}
-                          {i : b ⟶ c} {f : b ⟶ a}
+             {r' : c ⟶ d} {i : b ⟶ c} {f : b ⟶ a}
               {r : c ⟶ d} {q : b ⟶ c} {p : a ⟶ b}
-              {g : d ⟶ c} {h : c ⟶ b}
+              {g : d ⟶ c} {h : c ⟶ b} {p' : a ⟶ b}
                    {x : b ⟶ d} {z : a ⟶ c}
                    {y : d ⟶ b} {w : c ⟶ a}
   variable [Hq : is_iso q] include Hq
 
-  definition comp_eq_of_eq_inverse_comp (H : y = q⁻¹ ∘ g) : q ∘ y = g :=
+  theorem comp_eq_of_eq_inverse_comp (H : y = q⁻¹ ∘ g) : q ∘ y = g :=
   H⁻¹ ▸ comp_inverse_cancel_left q g
-  definition comp_eq_of_eq_comp_inverse (H : w = f ∘ q⁻¹) : w ∘ q = f :=
+  theorem comp_eq_of_eq_comp_inverse (H : w = f ∘ q⁻¹) : w ∘ q = f :=
   H⁻¹ ▸ inverse_comp_cancel_right f q
-  definition eq_comp_of_inverse_comp_eq (H : q⁻¹ ∘ g = y) : g = q ∘ y :=
+  theorem eq_comp_of_inverse_comp_eq (H : q⁻¹ ∘ g = y) : g = q ∘ y :=
   (comp_eq_of_eq_inverse_comp H⁻¹)⁻¹
-  definition eq_comp_of_comp_inverse_eq (H : f ∘ q⁻¹ = w) : f = w ∘ q :=
+  theorem eq_comp_of_comp_inverse_eq (H : f ∘ q⁻¹ = w) : f = w ∘ q :=
   (comp_eq_of_eq_comp_inverse H⁻¹)⁻¹
   variable {Hq}
-  definition inverse_comp_eq_of_eq_comp (H : z = q ∘ p) : q⁻¹ ∘ z = p :=
+  theorem inverse_comp_eq_of_eq_comp (H : z = q ∘ p) : q⁻¹ ∘ z = p :=
   H⁻¹ ▸ inverse_comp_cancel_left q p
-  definition comp_inverse_eq_of_eq_comp (H : x = r ∘ q) : x ∘ q⁻¹ = r :=
+  theorem comp_inverse_eq_of_eq_comp (H : x = r ∘ q) : x ∘ q⁻¹ = r :=
   H⁻¹ ▸ comp_inverse_cancel_right r q
-  definition eq_inverse_comp_of_comp_eq (H : q ∘ p = z) : p = q⁻¹ ∘ z :=
+  theorem eq_inverse_comp_of_comp_eq (H : q ∘ p = z) : p = q⁻¹ ∘ z :=
   (inverse_comp_eq_of_eq_comp H⁻¹)⁻¹
-  definition eq_comp_inverse_of_comp_eq (H : r ∘ q = x) : r = x ∘ q⁻¹ :=
+  theorem eq_comp_inverse_of_comp_eq (H : r ∘ q = x) : r = x ∘ q⁻¹ :=
   (comp_inverse_eq_of_eq_comp H⁻¹)⁻¹
 
-  definition eq_inverse_of_comp_eq_id' (H : h ∘ q = id) : h = q⁻¹ := (inverse_eq_left H)⁻¹
+  theorem eq_inverse_of_comp_eq_id' (H : h ∘ q = id) : h = q⁻¹ := (inverse_eq_left H)⁻¹
-  definition eq_inverse_of_comp_eq_id (H : q ∘ h = id) : h = q⁻¹ := (inverse_eq_right H)⁻¹
+  theorem eq_inverse_of_comp_eq_id (H : q ∘ h = id) : h = q⁻¹ := (inverse_eq_right H)⁻¹
-  definition inverse_eq_of_id_eq_comp (H : id = h ∘ q) : q⁻¹ = h :=
+  theorem inverse_eq_of_id_eq_comp (H : id = h ∘ q) : q⁻¹ = h :=
   (eq_inverse_of_comp_eq_id' H⁻¹)⁻¹
-  definition inverse_eq_of_id_eq_comp' (H : id = q ∘ h) : q⁻¹ = h :=
+  theorem inverse_eq_of_id_eq_comp' (H : id = q ∘ h) : q⁻¹ = h :=
   (eq_inverse_of_comp_eq_id H⁻¹)⁻¹
   variable [Hq]
-  definition eq_of_comp_inverse_eq_id (H : i ∘ q⁻¹ = id) : i = q :=
+  theorem eq_of_comp_inverse_eq_id (H : i ∘ q⁻¹ = id) : i = q :=
   eq_inverse_of_comp_eq_id' H ⬝ inverse_involutive q
-  definition eq_of_inverse_comp_eq_id (H : q⁻¹ ∘ i = id) : i = q :=
+  theorem eq_of_inverse_comp_eq_id (H : q⁻¹ ∘ i = id) : i = q :=
   eq_inverse_of_comp_eq_id H ⬝ inverse_involutive q
-  definition eq_of_id_eq_comp_inverse (H : id = i ∘ q⁻¹) : q = i := (eq_of_comp_inverse_eq_id H⁻¹)⁻¹
+  theorem eq_of_id_eq_comp_inverse (H : id = i ∘ q⁻¹) : q = i := (eq_of_comp_inverse_eq_id H⁻¹)⁻¹
-  definition eq_of_id_eq_inverse_comp (H : id = q⁻¹ ∘ i) : q = i := (eq_of_inverse_comp_eq_id H⁻¹)⁻¹
+  theorem eq_of_id_eq_inverse_comp (H : id = q⁻¹ ∘ i) : q = i := (eq_of_inverse_comp_eq_id H⁻¹)⁻¹
+
+  variables (q)
+  theorem comp.cancel_left  (H : q ∘ p = q ∘ p') : p = p' :=
+  by rewrite [-inverse_comp_cancel_left q, H, inverse_comp_cancel_left q]
+  theorem comp.cancel_right (H : r ∘ q = r' ∘ q) : r = r' :=
+  by rewrite [-comp_inverse_cancel_right _ q, H, comp_inverse_cancel_right _ q]
   end
 end iso

hott/algebra/category/limits.hlean

@@ -180,7 +180,8 @@ namespace category
   definition product_object : D :=
   limit_object (c2_functor D d d')
 
-  infixr × := product_object
+  infixr `×l`:30 := product_object
+  local infixr × := product_object
 
   definition pr1 : d × d' ⟶ d :=
   limit_morphism (c2_functor D d d') ff
@@ -340,4 +341,8 @@ namespace category
 
   end pullbacks
 
+  namespace ops
+  infixr × := product_object
+  end ops
+
 end category

hott/algebra/category/nat_trans.hlean

@@ -177,7 +177,7 @@ namespace nat_trans
   nat_trans.mk (λc, hom_of_eq (ap010 to_fun_ob p c))
                (λa b f, eq.rec_on p (!id_right ⬝ !id_left⁻¹))
 
-  definition compose_rev (θ : F ⟹ G) (η : G ⟹ H) : F ⟹ H := η ∘n θ
+  definition compose_rev [unfold-full] (θ : F ⟹ G) (η : G ⟹ H) : F ⟹ H := η ∘n θ
 
 end nat_trans
 

hott/homotopy/circle.hlean

@@ -167,7 +167,7 @@ namespace circle
     from λA a p, calc
       p   = ap (circle.elim a p) loop : elim_loop
       ... = ap (circle.elim a p) (refl base) : by rewrite H,
-  absurd H2 eq_bnot_ne_idp
+  eq_bnot_ne_idp H2
 
   definition nonidp (x : circle) : x = x :=
   begin

hott/homotopy/sphere.hlean

@@ -40,6 +40,7 @@ namespace sphere_index
   postfix `.+2`:(max+1) := λ(n : sphere_index), (n .+1 .+1)
   notation `-1` := minus_one
   export [coercions] nat
+  notation `ℕ₋₁` := sphere_index
 
   definition add (n m : sphere_index) : sphere_index :=
   sphere_index.rec_on m n (λ k l, l .+1)

hott/init/trunc.hlean

@@ -31,6 +31,7 @@ namespace is_trunc
   notation `-2` := trunc_index.minus_two
   notation `-1` := -2.+1 -- ISSUE: -1 gets printed as -2.+1
   export [coercions] nat
+  notation `ℕ₋₂` := trunc_index
 
   namespace trunc_index
   definition add (n m : trunc_index) : trunc_index :=

hott/init/types.hlean

@@ -51,6 +51,7 @@ end sigma
 namespace sum
   infixr ⊎ := sum
   infixr + := sum
+  infixr [parsing-only] `+t`:25 := sum -- notation which is never overloaded
   namespace low_precedence_plus
     reserve infixr ` + `:25  -- conflicts with notation for addition
     infixr ` + ` := sum
@@ -83,6 +84,7 @@ namespace prod
   -- notation for n-ary tuples
   notation `(` h `, ` t:(foldl `,` (e r, prod.mk r e) h) `)` := t
   infixr × := prod
+  infixr [parsing-only] `×t`:30 := prod -- notation which is never overloaded
 
   namespace ops
   infixr [parsing_only] * := prod