chore(library/hott): change precategory to structure, fix morphism.lean

library/hott/algebra/precategory/basic.lean

@@ -6,46 +6,30 @@ import hott.axioms.funext hott.trunc hott.equiv
 
 open path truncation
 
-inductive precategory [class] (ob : Type) : Type :=
-mk : Π (hom : ob → ob → Type)
-       (homH : Π {a b : ob}, is_hset (hom a b))
-       (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) →
-         precategory ob
+structure precategory [class] (ob : Type) : Type :=
+  (hom : ob → ob → Type)
+  (homH : Π {a b : ob}, is_hset (hom a b))
+  (comp : Π⦃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),
+     comp h (comp g f) ≈ comp (comp h g) f)
+  (id_left : Π ⦃a b : ob⦄ (f : hom a b), comp !ID f ≈ f)
+  (id_right : Π ⦃a b : ob⦄ (f : hom a b), comp f !ID ≈ f)
 
 namespace precategory
   variables {ob : Type} [C : precategory ob]
   variables {a b c d : ob}
   include C
 
-  definition hom [reducible] : ob → ob → Type := rec (λ hom homH compose id assoc idr idl, hom) C
+  definition compose := comp
 
-  definition homH [instance] : Π {a b : ob}, is_hset (hom a b) := rec (λ hom homH compose id assoc idr idl, homH) 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 homH compose id assoc idr idl, compose) C
-
-  definition id [reducible] : Π {a : ob}, hom a a := rec (λ hom homH 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 homH comp id assoc idr idl, assoc) C
-
-  theorem id_left  : Π ⦃a b : ob⦄ (f : hom a b), id ∘ f ≈ f :=
-  rec (λ hom homH comp id assoc idl idr, idl) C
-  theorem id_right : Π ⦃a b : ob⦄ (f : hom a b), f ∘ id ≈ f :=
-  rec (λ hom homH 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

library/hott/algebra/precategory/morphism.lean

@@ -58,7 +58,7 @@ namespace morphism
   calc
     g ≈ g ∘ id : !id_right
      ... ≈ g ∘ f ∘ g' : Hr
-     ... ≈ (g ∘ f) ∘ g' : assoc
+     ... ≈ (g ∘ f) ∘ g' : !assoc
      ... ≈ id ∘ g' : Hl
      ... ≈ g' : id_left
 
@@ -99,21 +99,26 @@ namespace morphism
 
   theorem composition_is_section [instance] [Hf : is_section f] [Hg : is_section g]
       : is_section (g ∘ f) :=
+  have aux : retraction_of g ∘ g ∘ f ≈ (retraction_of g ∘ g) ∘ f,
+    from !assoc,
   is_section.mk
     (calc
       (retraction_of f ∘ retraction_of g) ∘ g ∘ f
-            ≈ retraction_of f ∘ retraction_of g ∘ g ∘ f : assoc _ _ (g ∘ f)
-        ... ≈ retraction_of f ∘ (retraction_of g ∘ g) ∘ f : assoc _ g f
-        ... ≈ retraction_of f ∘ id ∘ f : retraction_compose g
+            ≈ retraction_of f ∘ retraction_of g ∘ g ∘ f : assoc
+        ... ≈ retraction_of f ∘ ((retraction_of g ∘ g) ∘ f) : aux
+        ... ≈ retraction_of f ∘ id ∘ f : {retraction_compose g}
         ... ≈ retraction_of f ∘ f : id_left f
-        ... ≈ id : retraction_compose)
+        ... ≈ id : retraction_compose f)
 
   theorem composition_is_retraction [instance] (Hf : is_retraction f) (Hg : is_retraction g)
       : is_retraction (g ∘ f) :=
+  have aux : f ∘ section_of f ∘ section_of g ≈ (f ∘ section_of f) ∘ section_of g,
+    from !assoc,
   is_retraction.mk
     (calc
-      (g ∘ f) ∘ section_of f ∘ section_of g ≈ g ∘ f ∘ section_of f ∘ section_of g : assoc
-        ... ≈ g ∘ (f ∘ section_of f) ∘ section_of g : assoc f _ _
+      (g ∘ f) ∘ section_of f ∘ section_of g
+            ≈ g ∘ f ∘ section_of f ∘ section_of g : assoc
+        ... ≈ g ∘ (f ∘ section_of f) ∘ section_of g : aux
         ... ≈ g ∘ id ∘ section_of g : compose_section f
         ... ≈ g ∘ section_of g : id_left (section_of g)
         ... ≈ id : compose_section)
@@ -181,14 +186,18 @@ namespace morphism
   theorem composition_is_mono [instance] [Hf : is_mono f] [Hg : is_mono g] : is_mono (g ∘ f) :=
   is_mono.mk
     (λ d h₁ h₂ H,
-    have H2 : g ∘ (f ∘ h₁) ≈ g ∘ (f ∘ h₂), from (assoc g f h₁)⁻¹  ▹ (assoc g f h₂)⁻¹ ▹ H,
-    mono_elim (mono_elim H2))
+      have H2 : g ∘ (f ∘ h₁) ≈ g ∘ (f ∘ h₂),
+        from calc g ∘ (f ∘ h₁) ≈ (g ∘ f) ∘ h₁ : !assoc
+                          ... ≈ (g ∘ f) ∘ h₂ : H
+                          ... ≈ g ∘ (f ∘ h₂) : !assoc, mono_elim (mono_elim H2))
 
   theorem composition_is_epi  [instance] [Hf : is_epi f] [Hg : is_epi g] : is_epi  (g ∘ f) :=
   is_epi.mk
     (λ d h₁ h₂ H,
-    have H2 : (h₁ ∘ g) ∘ f ≈ (h₂ ∘ g) ∘ f, from assoc h₁ g f  ▹ assoc h₂ g f ▹ H,
-    epi_elim (epi_elim H2))
+      have H2 : (h₁ ∘ g) ∘ f ≈ (h₂ ∘ g) ∘ f,
+        from calc (h₁ ∘ g) ∘ f ≈ h₁ ∘ g ∘ f : !assoc
+                          ... ≈ h₂ ∘ g ∘ f : H
+                          ... ≈ (h₂ ∘ g) ∘ f: !assoc, epi_elim (epi_elim H2))
 
 end morphism
 namespace morphism