feat(category): start with the introduction rule for equivalences

hott/algebra/category/adjoint.hlean

@@ -2,6 +2,10 @@
 Copyright (c) 2015 Floris van Doorn. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Floris van Doorn
+
+Properties of functors such as adjoint functors, equivalences, faithful or full functors
+
+TODO: Split this file in different files
 -/
 
 import algebra.category.constructions function arity
@@ -225,16 +229,40 @@ namespace category
   theorem reflect_inverse (F : C ⇒ D) [H : fully_faithful F] {c c' : C} (f : c ⟶ c')
     [H : is_iso f] : (to_fun_hom F)⁻¹ᶠ (F f)⁻¹ = f⁻¹ :=
   inverse_eq_inverse (idp : to_hom (@(iso.mk f) (reflect_is_iso F f)) = f)
+end category
 
-/-
+namespace category
   section
-    variables (η : Πc, G (F c) ≅ c) (ε : Πd, F (G d) ≅ d) -- we need some kind of naturality
-    include η ε
-    --definition inverse_of_unit_counit
+    parameters {C D : Precategory} {F : C ⇒ D} {G : D ⇒ C} (η : G ∘f F ≅ 1) (ε : F ∘f G ≅ 1)
 
-     private definition adj_η (c : C) : G (F c) ≅ c :=
-     to_fun_iso G (to_fun_iso F (η c)⁻¹ⁱ) ⬝i to_fun_iso G (ε (F c)) ⬝i η c
-     open iso
+      -- 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ε : Π⦃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 : F ∘f G ⟹ 1 := to_hom ε
+
+     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' (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
+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) :
        to_hom (ε (F c)) ∘ F (to_hom (adj_η η ε c)⁻¹ⁱ) = id  :=
@@ -248,16 +276,88 @@ namespace category
        exact sorry
      end
 
+    attribute functor.id [reducible]
     variables (F G)
     definition is_equivalence.mk : is_equivalence F :=
     begin
-      fconstructor,
+      fapply is_equivalence.mk',
       { exact G},
-      { }
+      { 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
 
+  definition is_equivalence.mk2 (η : G ∘f F ≅ 1) (ε : F ∘f G ≅ 1) : is_equivalence F :=
+  is_equivalence.mk F G
+    (componentwise_iso η) (componentwise_iso ε)
+    begin intro c c' f, esimp, apply naturality (to_hom η) f end
+    begin intro c c' f, esimp, apply naturality (to_hom ε) f end
+
+exit
+
+  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_η η ε)},
+      { exact to_hom ε},
+      { exact adjointify_adjH η ε},
+      { exact adjointify_adjK η ε},
+      { unfold to_inv, apply is_iso_inverse},
+      { apply iso.struct},
+    end
+
+  end
+/-
+
   definition fully_faithful_of_is_equivalence (F : C ⇒ D) [H : is_equivalence F]
     : fully_faithful F :=
   begin

hott/algebra/category/constructions/functor.hlean

@@ -35,14 +35,14 @@ namespace category
   nat_trans.mk
     (λc, (η c)⁻¹)
     (λc d f,
-    begin
+    abstract begin
       apply comp_inverse_eq_of_eq_comp,
       transitivity (natural_map η d)⁻¹ ∘ to_fun_hom G f ∘ natural_map η c,
         {apply eq_inverse_comp_of_comp_eq, symmetry, apply naturality},
         {apply assoc}
-    end)
+    end end)
 
-  definition nat_trans_left_inverse : nat_trans_inverse η ∘n η = nat_trans.id :=
+  definition nat_trans_left_inverse : nat_trans_inverse η ∘n η = 1 :=
   begin
     fapply (apd011 nat_trans.mk),
       apply eq_of_homotopy, intro c, apply left_inverse,
@@ -50,7 +50,7 @@ namespace category
     apply is_hset.elim
   end
 
-  definition nat_trans_right_inverse : η ∘n nat_trans_inverse η = nat_trans.id :=
+  definition nat_trans_right_inverse : η ∘n nat_trans_inverse η = 1 :=
   begin
     fapply (apd011 nat_trans.mk),
       apply eq_of_homotopy, intro c, apply right_inverse,
@@ -69,9 +69,9 @@ namespace category
 
   section
   /- and conversely, if a natural transformation is an iso, it is componentwise an iso -/
-  variables {A B C D : Precategory} {F G : D ^c C} (η : hom F G) [isoη : is_iso η] (c : C)
+  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] : is_iso (η c) :=
+  definition componentwise_is_iso [instance] [constructor] : is_iso (η c) :=
   @is_iso.mk _ _ _ _ _ (natural_map η⁻¹ c) (ap010 natural_map ( left_inverse η) c)
                                            (ap010 natural_map (right_inverse η) c)
 
@@ -113,19 +113,19 @@ namespace category
     : natural_map (inv_of_eq p) c = hom_of_eq (ap010 to_fun_ob p c)⁻¹ :=
   eq.rec_on p idp
 
-  definition hom_of_eq_compose_right {H : C ^c B} (p : F = G)
+  definition hom_of_eq_compose_right {H : B ⇒ C} (p : F = G)
     : hom_of_eq (ap (λx, x ∘f H) p) = hom_of_eq p ∘nf H :=
   eq.rec_on p idp
 
-  definition inv_of_eq_compose_right {H : C ^c B} (p : F = G)
+  definition inv_of_eq_compose_right {H : B ⇒ C} (p : F = G)
     : inv_of_eq (ap (λx, x ∘f H) p) = inv_of_eq p ∘nf H :=
   eq.rec_on p idp
 
-  definition hom_of_eq_compose_left {H : B ^c D} (p : F = G)
+  definition hom_of_eq_compose_left {H : D ⇒ C} (p : F = G)
     : hom_of_eq (ap (λx, H ∘f x) p) = H ∘fn hom_of_eq p :=
   by induction p; exact !fn_id⁻¹
 
-  definition inv_of_eq_compose_left {H : B ^c D} (p : F = G)
+  definition inv_of_eq_compose_left {H : D ⇒ C} (p : F = G)
     : inv_of_eq (ap (λx, H ∘f x) p) = H ∘fn inv_of_eq p :=
   by induction p; exact !fn_id⁻¹
 

hott/algebra/category/constructions/product.hlean

@@ -3,7 +3,7 @@ Copyright (c) 2015 Floris van Doorn. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Floris van Doorn, Jakob von Raumer
 
-Functor product precategory and (TODO) category
+Product precategory and (TODO) category
 -/
 
 import ..category ..functor hit.trunc

hott/algebra/category/constructions/sum.hlean

@@ -3,7 +3,7 @@ Copyright (c) 2015 Floris van Doorn. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Floris van Doorn, Jakob von Raumer
 
-Functor product precategory and (TODO) category
+Sum precategory and (TODO) category
 -/
 
 import ..category ..functor types.sum

hott/algebra/category/iso.hlean

@@ -50,7 +50,7 @@ namespace iso
   definition is_iso_id [instance] [priority 500] (a : ob) : is_iso (ID a) :=
   is_iso.mk !id_id !id_id
 
-  definition is_iso_inverse [instance] [priority 200] (f : a ⟶ b) [H : is_iso f] : is_iso f⁻¹ :=
+  definition is_iso_inverse [instance] [priority 200] (f : a ⟶ b) {H : is_iso f} : is_iso f⁻¹ :=
   is_iso.mk !right_inverse !left_inverse
 
   definition left_inverse_eq_right_inverse {f : a ⟶ b} {g g' : hom b a}
@@ -165,6 +165,12 @@ namespace iso
   infixl ` ⬝i `:75 := iso.trans
   postfix [parsing_only] `⁻¹ⁱ`:(max + 1) := iso.symm
 
+  definition change_hom (H : a ≅ b) (f : a ⟶ b) (p : to_hom H = f) : a ≅ b :=
+  iso.MK f (to_inv H) (p ▸ to_left_inverse H) (p ▸ to_right_inverse H)
+
+  definition change_inv (H : a ≅ b) (g : b ⟶ a) (p : to_inv H = g) : a ≅ b :=
+  iso.MK (to_hom H) g (p ▸ to_left_inverse H) (p ▸ to_right_inverse H)
+
   definition iso_mk_eq {f f' : a ⟶ b} [H : is_iso f] [H' : is_iso f'] (p : f = f')
       : iso.mk f = iso.mk f' :=
   apd011 iso.mk p !is_hprop.elim
@@ -279,6 +285,10 @@ namespace iso
 
 end iso
 
+attribute iso.refl [refl]
+attribute iso.symm [symm]
+attribute iso.trans [trans]
+
 namespace iso
   /-
   rewrite lemmas for inverses, modified from

hott/algebra/category/nat_trans.hlean

@@ -175,4 +175,9 @@ 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 θ
+
 end nat_trans
+
+attribute nat_trans.compose_rev [trans] -- TODO: this doesn't work
+attribute nat_trans.id [refl]

hott/algebra/e_closure.hlean

@@ -4,7 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Floris van Doorn
 
 The "equivalence closure" of a type-valued relation.
-Given a binary type-valued relation (fibration), we add reflexivity, symmetry and transitivity terms
+A more appropriate intuition is the type of words formed from the relation,
+  and inverses, concatenations and reflexivity
 -/
 
 import .relation eq2 arity

src/emacs/lean-input.el

@@ -412,10 +412,10 @@ order for the change to take effect."
   ("ur" . ,(lean-input-to-string-list "↗⇗                                         ➶➹➚                             "))
   ("dr" . ,(lean-input-to-string-list "↘⇘                        ⇲                ➴➷➘                             "))
   ("dl" . ,(lean-input-to-string-list "↙⇙                                                                         "))
-  ("==>" . ("⟹"))
+  ("==>" . ("⟹")) ("nattrans" . ("⟹")) ("nat_trans" . ("⟹"))
 
   ("l-"  . ("←"))  ("<-"  . ("←"))  ("l="  . ("⇐"))
-  ("r-"  . ("→"))  ("->"  . ("→"))  ("r="  . ("⇒"))  ("=>"  . ("⇒"))
+  ("r-"  . ("→"))  ("->"  . ("→"))  ("r="  . ("⇒"))  ("=>"  . ("⇒")) ("functor"  . ("⇒"))
   ("u-"  . ("↑"))                   ("u="  . ("⇑"))
   ("d-"  . ("↓"))                   ("d="  . ("⇓"))
   ("ud-" . ("↕"))                   ("ud=" . ("⇕"))