From b62b4754cbdf2eb715b4c082061e56fd466f6ff2 Mon Sep 17 00:00:00 2001
From: Floris van Doorn <fpv@andrew.cmu.edu>
Date: Mon, 24 Nov 2014 20:24:30 -0500
Subject: [PATCH] feat(library/algebra): modify categories to use definitions,
 prove basic theorems about discrete categories

---
 library/algebra/category/adjoint.lean       | 21 +-----
 library/algebra/category/basic.lean         | 54 +++++---------
 library/algebra/category/constructions.lean | 80 ++++++++++++---------
 library/algebra/category/functor.lean       | 72 ++++++-------------
 4 files changed, 88 insertions(+), 139 deletions(-)

diff --git a/library/algebra/category/adjoint.lean b/library/algebra/category/adjoint.lean
index fb858f2ae..7b295500e 100644
--- a/library/algebra/category/adjoint.lean
+++ b/library/algebra/category/adjoint.lean
@@ -7,26 +7,11 @@ import .constructions
 open eq eq.ops category functor natural_transformation category.ops prod category.product
 
 namespace adjoint
---representable functor
-
-  definition foo (C : Category) : C ×c C ⇒ C ×c C := functor.id
 
   -- definition Hom (C : Category) : Cᵒᵖ ×c C ⇒ type :=
   -- functor.mk (λ a, hom (pr1 a) (pr2 a))
-  --            (λ a b f h, pr2 f ∘ h ∘ pr1 f)
-  --            (λ a, funext (λh, !id_left ⬝ !id_right))
-  --            (λ a b c g f, funext (λh,
-  --   show (pr2 g ∘ pr2 f) ∘ h ∘ (pr1 f ∘ pr1 g) = pr2 g ∘ (pr2 f ∘ h ∘ pr1 f) ∘ pr1 g, from sorry))
-  --I'm lazy, waiting for automation to fill this
+  --            (λ a b f h, sorry)
+  --            (λ a, sorry)
+  --            (λ a b c g f, sorry)
 
-  variables (C D : Category)
-
-  -- private definition aux_prod_cat [instance] : category (obD × obD) := prod_category (opposite.opposite D) D
-
---   definition adjoint.{l} (F : C ⇒ D) (G : D ⇒ C) := 
---   --@natural_transformation _ Type.{l} (Dᵒᵖ ×c D) type_category.{l+1} (Hom D) (Hom D)
--- sorry
---(@functor.compose _ _ _ _ _ _ (Hom D) (@product.prod_functor _ _ _ _ _ _ (Dᵒᵖ) D sorry sorry))
-                       --(Hom C ∘f sorry)
-  --product.prod_functor (opposite.opposite_functor F) (functor.ID D)
 end adjoint
diff --git a/library/algebra/category/basic.lean b/library/algebra/category/basic.lean
index b99f6487d..7a69c90af 100644
--- a/library/algebra/category/basic.lean
+++ b/library/algebra/category/basic.lean
@@ -6,44 +6,25 @@ import logic.axioms.funext
 
 open eq eq.ops
 
-inductive category [class] (ob : Type) : Type :=
-mk : Π (hom : ob → ob → Type)
-       (comp : Π⦃a b c : ob⦄, hom b c → hom a b → hom a c)
-       (id : Π {a : ob}, hom a a),
-       (Π ⦃a b c d : ob⦄ {h : hom c d} {g : hom b c} {f : hom a b},
-           comp h (comp g f) = comp (comp h g) f) →
-       (Π ⦃a b : ob⦄ {f : hom a b}, comp id f = f) →
-       (Π ⦃a b : ob⦄ {f : hom a b}, comp f id = f) →
-         category ob
+structure category [class] (ob : Type) : Type :=
+  (hom : ob → ob → Type)
+  (compose : Π⦃a b c : ob⦄, hom b c → hom a b → hom a c)
+  (ID : Π (a : ob), hom a a)
+  (assoc : Π ⦃a b c d : ob⦄ (h : hom c d) (g : hom b c) (f : hom a b),
+     compose h (compose g f) = compose (compose h g) f)
+  (id_left : Π ⦃a b : ob⦄ (f : hom a b), compose !ID f = f)
+  (id_right : Π ⦃a b : ob⦄ (f : hom a b), compose f !ID = f)
 
 namespace category
   variables {ob : Type} [C : category ob]
-  variables {a b c d : ob}
+  variables {a b c d : ob} {h : hom c d} {g : hom b c} {f : hom a b} {i : hom a a}
   include C
 
-  definition hom [reducible] : ob → ob → Type := rec (λ hom compose id assoc idr idl, hom) C
-  -- note: needs to be reducible to typecheck composition in opposite category
-  definition compose [reducible] : Π {a b c : ob}, hom b c → hom a b → hom a c :=
-  rec (λ hom compose id assoc idr idl, compose) C
-
-  definition id [reducible] : Π {a : ob}, hom a a := rec (λ hom compose id assoc idr idl, id) C
-  definition ID [reducible] (a : ob) : hom a a := id
+  definition id [reducible] {a : ob} : hom a a := ID a
 
   infixr `∘` := compose
   infixl `⟶`:25 := hom -- input ⟶ using \--> (this is a different arrow than \-> (→))
 
-  variables {h : hom c d} {g : hom b c} {f : hom a b} {i : hom a a}
-
-  theorem assoc : Π ⦃a b c d : ob⦄ (h : hom c d) (g : hom b c) (f : hom a b),
-      h ∘ (g ∘ f) = (h ∘ g) ∘ f :=
-  rec (λ hom comp id assoc idr idl, assoc) C
-
-  theorem id_left  : Π ⦃a b : ob⦄ (f : hom a b), id ∘ f = f :=
-  rec (λ hom comp id assoc idl idr, idl) C
-  theorem id_right : Π ⦃a b : ob⦄ (f : hom a b), f ∘ id = f :=
-  rec (λ hom comp id assoc idl idr, idr) C
-
-  --the following is the only theorem for which "include C" is necessary if C is a variable (why?)
   theorem id_compose (a : ob) : (ID a) ∘ id = id := !id_left
 
   theorem left_id_unique (H : Π{b} {f : hom b a}, i ∘ f = f) : i = id :=
@@ -55,18 +36,15 @@ namespace category
      ... = id     : H
 end category
 
-inductive Category : Type := mk : Π (ob : Type), category ob → Category
+structure Category : Type :=
+  (objects : Type)
+  (category_instance : category objects)
 
 namespace category
   definition Mk {ob} (C) : Category := Category.mk ob C
-  definition MK (a b c d e f g) : Category := Category.mk a (category.mk b c d e f g)
-
-  definition objects [coercion] [reducible] (C : Category) : Type
-  := Category.rec (fun c s, c) C
-
-  definition category_instance [instance] [coercion] [reducible] (C : Category) : category (objects C)
-  := Category.rec (fun c s, s) C
-
+  definition MK (o h c i a l r) : Category := Category.mk o (category.mk h c i a l r)
+  definition objects [coercion] [reducible] := Category.objects
+  definition category_instance [instance] [coercion] [reducible] := Category.category_instance
 end category
 
 open category
diff --git a/library/algebra/category/constructions.lean b/library/algebra/category/constructions.lean
index cd7ddaaa4..9de421d75 100644
--- a/library/algebra/category/constructions.lean
+++ b/library/algebra/category/constructions.lean
@@ -12,7 +12,7 @@ open eq eq.ops prod
 namespace category
   namespace opposite
   section
-  definition opposite {ob : Type} (C : category ob) : category ob :=
+  definition opposite [reducible] {ob : Type} (C : category ob) : category ob :=
   mk (λa b, hom b a)
      (λ a b c f g, g ∘ f)
      (λ a, id)
@@ -20,7 +20,7 @@ namespace category
      (λ a b f, !id_right)
      (λ a b f, !id_left)
 
-  definition Opposite (C : Category) : Category := Mk (opposite C)
+  definition Opposite [reducible] (C : Category) : Category := Mk (opposite C)
   --direct construction:
   -- MK C
   --    (λa b, hom b a)
@@ -45,7 +45,7 @@ namespace category
   end
   end opposite
 
-  definition type_category : category Type :=
+  definition type_category [reducible] : category Type :=
   mk (λa b, a → b)
      (λ a b c, function.compose)
      (λ a, function.id)
@@ -53,15 +53,15 @@ namespace category
      (λ a b f, function.compose_id_left f)
      (λ a b f, function.compose_id_right f)
 
-  definition Type_category : Category := Mk type_category
+  definition Type_category [reducible] : Category := Mk type_category
 
   section
   open decidable unit empty
   variables {A : Type} [H : decidable_eq A]
   include H
-  definition set_hom (a b : A) := decidable.rec_on (H a b) (λh, unit) (λh, empty)
+  definition set_hom [reducible] (a b : A) := decidable.rec_on (H a b) (λh, unit) (λh, empty)
   theorem set_hom_subsingleton [instance] (a b : A) : subsingleton (set_hom a b) := _
-  definition set_compose {a b c : A} (g : set_hom b c) (f : set_hom a b) : set_hom a c :=
+  definition set_compose [reducible] {a b c : A} (g : set_hom b c) (f : set_hom a b) : set_hom a c :=
   decidable.rec_on
     (H b c)
     (λ Hbc g, decidable.rec_on
@@ -78,6 +78,21 @@ namespace category
      (λ a b f, @subsingleton.elim (set_hom a b) _ _ _)
      (λ a b f, @subsingleton.elim (set_hom a b) _ _ _)
   definition Discrete_category (A : Type) [H : decidable_eq A] := Mk (discrete_category A)
+    context
+    instance discrete_category
+    include H
+    theorem dicrete_category.endomorphism {a b : A} (f : a ⟶ b) : a = b :=
+    decidable.rec_on (H a b) (λh f, h) (λh f, empty.rec _ f) f
+
+    theorem dicrete_category.discrete {a b : A} (f : a ⟶ b)
+      : eq.rec_on (dicrete_category.endomorphism f) f = (ID b) :=
+    @subsingleton.elim _ !set_hom_subsingleton _ _
+
+    definition discrete_category.rec_on {P : Πa b, a ⟶ b → Type} {a b : A} (f : a ⟶ b)
+        (H : ∀a, P a a id) : P a b f :=
+    cast (dcongr_arg3 P rfl (dicrete_category.endomorphism f⁻¹)
+                            (@subsingleton.elim _ !set_hom_subsingleton _ _) ⁻¹) (H a)
+    end
   end
   section
   open unit bool
@@ -88,49 +103,49 @@ namespace category
   end
 
   namespace product
-  section
-  open prod
-  definition prod_category {obC obD : Type} (C : category obC) (D : category obD)
-      : category (obC × obD) :=
-  mk (λa b, hom (pr1 a) (pr1 b) × hom (pr2 a) (pr2 b))
-     (λ a b c g f, (pr1 g ∘ pr1 f , pr2 g ∘ pr2 f) )
-     (λ a, (id,id))
-     (λ a b c d h g f, pair_eq    !assoc    !assoc   )
-     (λ a b f,         prod.equal !id_left  !id_left )
-     (λ a b f,         prod.equal !id_right !id_right)
+    section
+    open prod
+    definition prod_category [reducible] {obC obD : Type} (C : category obC) (D : category obD)
+        : category (obC × obD) :=
+    mk (λa b, hom (pr1 a) (pr1 b) × hom (pr2 a) (pr2 b))
+       (λ a b c g f, (pr1 g ∘ pr1 f , pr2 g ∘ pr2 f) )
+       (λ a, (id,id))
+       (λ a b c d h g f, pair_eq    !assoc    !assoc   )
+       (λ a b f,         prod.equal !id_left  !id_left )
+       (λ a b f,         prod.equal !id_right !id_right)
 
-  definition Prod_category (C D : Category) : Category := Mk (prod_category C D)
-
-  end
+    definition Prod_category [reducible] (C D : Category) : Category := Mk (prod_category C D)
+    end
   end product
 
   namespace ops
     notation `type`:max := Type_category
-    notation 1 := Category_one --it was confusing for me (Floris) that no ``s are needed here
+    notation 1 := Category_one
     notation 2 := Category_two
     postfix `ᵒᵖ`:max := opposite.Opposite
     infixr `×c`:30 := product.Prod_category
-    instance [persistent] type_category category_one 
+    instance [persistent] type_category category_one
                           category_two product.prod_category
   end ops
 
   open ops
   namespace opposite
   section
-  open ops functor
-  definition opposite_functor {C D : Category} (F : C ⇒ D) : Cᵒᵖ ⇒ Dᵒᵖ :=
+  open functor
+  definition opposite_functor [reducible] {C D : Category} (F : C ⇒ D) : Cᵒᵖ ⇒ Dᵒᵖ :=
   @functor.mk (Cᵒᵖ) (Dᵒᵖ)
               (λ a, F a)
               (λ a b f, F f)
-              (λ a, !respect_id)
-              (λ a b c g f, !respect_comp)
+              (λ a, respect_id F a)
+              (λ a b c g f, respect_comp F f g)
   end
   end opposite
 
   namespace product
   section
   open ops functor
-  definition prod_functor {C C' D D' : Category} (F : C ⇒ D) (G : C' ⇒ D') : C ×c C' ⇒ D ×c D' :=
+  definition prod_functor [reducible] {C C' D D' : Category} (F : C ⇒ D) (G : C' ⇒ D')
+      : C ×c C' ⇒ D ×c D' :=
   functor.mk (λ a, pair (F (pr1 a)) (G (pr2 a)))
              (λ a b f, pair (F (pr1 f)) (G (pr2 f)))
              (λ a, pair_eq !respect_id !respect_id)
@@ -162,7 +177,7 @@ namespace category
   protected definition to_ob  (a : slice_obs C c) : ob              := dpr1 a
   protected definition to_ob_def (a : slice_obs C c) : to_ob a = dpr1 a := rfl
   protected definition ob_hom (a : slice_obs C c) : hom (to_ob a) c := dpr2 a
-  -- protected theorem slice_obs_equal (H₁ : to_ob a = to_ob b) 
+  -- protected theorem slice_obs_equal (H₁ : to_ob a = to_ob b)
   --     (H₂ : eq.drec_on H₁ (ob_hom a) = ob_hom b) : a = b :=
   -- sigma.equal H₁ H₂
 
@@ -191,7 +206,7 @@ namespace category
      (λ a b f,         sigma.equal !id_right !proof_irrel)
   -- We use !proof_irrel instead of rfl, to give the unifier an easier time
 
-  -- definition slice_category {ob : Type} (C : category ob) (c : ob) : category (Σ(b : ob), hom b c) 
+  -- definition slice_category {ob : Type} (C : category ob) (c : ob) : category (Σ(b : ob), hom b c)
   -- :=
   -- mk (λa b, Σ(g : hom (dpr1 a) (dpr1 b)), dpr2 b ∘ g = dpr2 a)
   --    (λ a b c g f, dpair (dpr1 g ∘ dpr1 f)
@@ -218,7 +233,7 @@ namespace category
              (λ a, rfl)
              (λ a b c g f, rfl)
 
-  definition postcomposition_functor {x y : D} (h : x ⟶ y) 
+  definition postcomposition_functor {x y : D} (h : x ⟶ y)
       : Slice_category D x ⇒ Slice_category D y :=
   functor.mk (λ a, dpair (to_ob a) (h ∘ ob_hom a))
              (λ a b f, dpair (hom_hom f)
@@ -232,9 +247,9 @@ namespace category
   -- definition heq2 {A B : Type} (H : A = B) (a : A) (b : B) := a == b
   -- definition heq2.intro {A B : Type} {a : A} {b : B} (H : a == b) : heq2 (heq.type_eq H) a b := H
   -- definition heq2.elim {A B : Type} {a : A} {b : B} (H : A = B) (H2 : heq2 H a b) : a == b := H2
-  -- definition heq2.proof_irrel {A B : Prop} (a : A) (b : B) (H : A = B) : heq2 H a b := 
+  -- definition heq2.proof_irrel {A B : Prop} (a : A) (b : B) (H : A = B) : heq2 H a b :=
   -- hproof_irrel H a b
-  -- theorem functor.mk_eq2 {C D : Category} {obF obG : C → D} {homF homG idF idG compF compG} 
+  -- theorem functor.mk_eq2 {C D : Category} {obF obG : C → D} {homF homG idF idG compF compG}
   --    (Hob : ∀x, obF x = obG x)
   --    (Hmor : ∀(a b : C) (f : a ⟶ b), heq2 (congr_arg (λ x, x a ⟶ x b) (funext Hob)) (homF a b f) (homG a b f))
   --      : functor.mk obF homF idF compF = functor.mk obG homG idG compG :=
@@ -345,8 +360,7 @@ namespace category
 
 end category
 
-  -- definition foo
-  --     : category (sorry) :=
+  -- definition foo : category (sorry) :=
   -- mk (λa b, sorry)
   --    (λ a b c g f, sorry)
   --    (λ a, sorry)
diff --git a/library/algebra/category/functor.lean b/library/algebra/category/functor.lean
index aaf7eb124..8bbc7fc9b 100644
--- a/library/algebra/category/functor.lean
+++ b/library/algebra/category/functor.lean
@@ -7,48 +7,43 @@ import logic.cast
 open function
 open category eq eq.ops heq
 
-inductive functor (C D : Category) : Type :=
-mk : Π (obF : C → D) (homF : Π(a b : C), hom a b → hom (obF a) (obF b)),
-    (Π (a : C), homF a a (ID a) = ID (obF a)) →
-    (Π (a b c : C) {g : hom b c} {f : hom a b}, homF a c (g ∘ f) = homF b c g ∘ homF a b f) →
-     functor C D
+structure functor (C D : Category) : Type :=
+  (object : C → D)
+  (morphism : Π⦃a b : C⦄, hom a b → hom (object a) (object b))
+  (respect_id : Π (a : C), morphism (ID a) = ID (object a))
+  (respect_comp : Π ⦃a b c : C⦄ (g : hom b c) (f : hom a b),
+      morphism (g ∘ f) = morphism g ∘ morphism f)
 
 infixl `⇒`:25 := functor
 
 namespace functor
-  variables {C D E : Category}
-  definition object [coercion] (F : functor C D) : C → D := rec (λ obF homF Hid Hcomp, obF) F
+  coercion [persistent] object
+  coercion [persistent] morphism
+  irreducible [persistent] respect_id respect_comp
 
-  definition morphism [coercion] (F : functor C D) : Π⦃a b : C⦄, hom a b → hom (F a) (F b) :=
-  rec (λ obF homF Hid Hcomp, homF) F
+  variables {A B C D : Category}
 
-  theorem respect_id (F : functor C D) : Π (a : C), F (ID a) = id :=
-  rec (λ obF homF Hid Hcomp, Hid) F
-
-  theorem respect_comp (F : functor C D) : Π ⦃a b c : C⦄ (g : hom b c) (f : hom a b),
-      F (g ∘ f) = F g ∘ F f :=
-  rec (λ obF homF Hid Hcomp, Hcomp) F
-
-  protected definition compose (G : functor D E) (F : functor C D) : functor C E :=
+  protected definition compose [reducible] (G : functor B C) (F : functor A B) : functor A C :=
   functor.mk
     (λx, G (F x))
     (λ a b f, G (F f))
-    (λ a, calc
-      G (F (ID a)) = G id : {respect_id F a} --not giving the braces explicitly makes the elaborator compute a couple more seconds
-               ... = id   : respect_id G (F a))
-    (λ a b c g f, calc
+    (λ a, proof calc
+      G (F (ID a)) = G id : {respect_id F a}
+      --not giving the braces explicitly makes the elaborator compute a couple more seconds
+               ... = id   : respect_id G (F a) qed)
+    (λ a b c g f, proof calc
       G (F (g ∘ f)) = G (F g ∘ F f)     : respect_comp F g f
-                ... = G (F g) ∘ G (F f) : respect_comp G (F g) (F f))
+                ... = G (F g) ∘ G (F f) : respect_comp G (F g) (F f) qed)
 
   infixr `∘f`:60 := compose
 
-  protected theorem assoc {A B C D : Category} (H : functor C D) (G : functor B C) (F : functor A B) :
+  protected theorem assoc (H : functor C D) (G : functor B C) (F : functor A B) :
       H ∘f (G ∘f F) = (H ∘f G) ∘f F :=
   rfl
 
-  protected definition id {C : Category} : functor C C :=
+  protected definition id [reducible] {C : Category} : functor C C :=
   mk (λa, a) (λ a b f, f) (λ a, rfl) (λ a b c f g, rfl)
-  protected definition ID (C : Category) : functor C C := id
+  protected definition ID [reducible] (C : Category) : functor C C := id
 
   protected theorem id_left  (F : functor C D) : id ∘f F = F :=
   functor.rec (λ obF homF idF compF, dcongr_arg4 mk rfl rfl !proof_irrel !proof_irrel) F
@@ -66,6 +61,7 @@ namespace category
      (λ a b c d h g f, !functor.assoc)
      (λ a b f, !functor.id_left)
      (λ a b f, !functor.id_right)
+
   definition Category_of_categories [reducible] := Mk category_of_categories
 
   namespace ops
@@ -75,32 +71,8 @@ namespace category
 end category
 
 namespace functor
---  open category.ops
---   universes l m
+
    variables {C D : Category}
---   check hom C D
---   variables (F : C ⟶ D) (G : D ⇒ C)
---   check G ∘ F
---   check F ∘f G
---   variables (a b : C) (f : a ⟶ b)
---   check F a
---   check F b
---   check F f
---   check G (F f)
---   print "---"
--- --  check (G ∘ F) f --error
---   check (λ(x : functor C C), x) (G ∘ F) f
---   check (G ∘f F) f
---   print "---"
--- --  check (G ∘ F) a --error
---   check (G ∘f F) a
---   print "---"
--- --  check λ(H : hom C D) (x : C), H x  --error
---   check λ(H : @hom _ Cat C D) (x : C), H x
---   check λ(H : C ⇒ D) (x : C), H x
---   print "---"
---   -- variables {obF obG : C → D} (Hob : ∀x, obF x = obG x) (homF : Π(a b : C) (f : a ⟶ b), obF a ⟶ obF b) (homG : Π(a b : C) (f : a ⟶ b), obG a ⟶ obG b)
--- --  check eq.rec_on (funext Hob) homF = homG
 
   theorem mk_heq {obF obG : C → D} {homF homG idF idG compF compG} (Hob : ∀x, obF x = obG x)
      (Hmor : ∀(a b : C) (f : a ⟶ b), homF a b f == homG a b f)