feat(library): add constructions of categories, some changes in eq, sigma and path

in eq, add theorem for proof irrelevance and congruence for binary functions
in sigma, add some support for triplets
in path, comment out two unneccesary definitions
in category, add Cat, slice, coslice, product and arrow categories, also add fully bundled approach

library/algebra/category.lean

@@ -6,20 +6,23 @@
 import logic.core.eq logic.core.connectives
 import data.unit data.sigma data.prod
 import algebra.function
+import logic.axioms.funext
 
 open eq
 
 inductive category [class] (ob : Type) : Type :=
-mk : Π (mor : ob → ob → Type) (comp : Π{A B C : ob}, mor B C → mor A B → mor A C)
+mk : Π (mor : ob → ob → Type) (comp : Π⦃A B C : ob⦄, mor B C → mor A B → mor A C)
            (id : Π {A : ob}, mor A A),
-            (Π {A B C D : ob} {f : mor A B} {g : mor B C} {h : mor C D},
+            (Π ⦃A B C D : ob⦄ {h : mor C D} {g : mor B C} {f : mor A B},
             comp h (comp g f) = comp (comp h g) f) →
-           (Π {A B : ob} {f : mor A B}, comp f id = f) →
+           (Π ⦃A B : ob⦄ {f : mor A B}, comp id f = f) →
-           (Π {A B : ob} {f : mor A B}, comp id f = f) →
+           (Π ⦃A B : ob⦄ {f : mor A B}, comp f id = f) →
             category ob
 
+inductive Category : Type :=
+mk : Π (A : Type), category A → Category
+
 namespace category
-  precedence `∘` : 60
 
   section
   parameters {ob : Type} {Cat : category ob} {A B C D : ob}
@@ -32,16 +35,17 @@ namespace category
   rec (λ mor compose id assoc idr idl, id) Cat
   definition ID (A : ob) : mor A A := @id A
 
+  precedence `∘` : 60
   infixr `∘` := compose
 
-  theorem assoc : Π {A B C D : ob} {f : mor A B} {g : mor B C} {h : mor C D},
+  theorem assoc : Π {A B C D : ob} {h : mor C D} {g : mor B C} {f : mor A B},
                 h ∘ (g ∘ f) = (h ∘ g) ∘ f :=
   rec (λ mor comp id assoc idr idl, assoc) Cat
 
-  theorem id_right : Π {A B : ob} {f : mor A B}, f ∘ id = f :=
-  rec (λ mor comp id assoc idr idl, idr) Cat
   theorem id_left  : Π {A B : ob} {f : mor A B}, id ∘ f = f :=
-  rec (λ mor comp id assoc idr idl, idl) Cat
+  rec (λ mor comp id assoc idl idr, idl) Cat
+  theorem id_right : Π {A B : ob} {f : mor A B}, f ∘ id = f :=
+  rec (λ mor comp id assoc idl idr, idr) Cat
 
   theorem id_compose {A : ob} : (ID A) ∘ id = id :=
   id_left
@@ -178,8 +182,16 @@ namespace category
   ... = h : id_right
 
   end
-  infixr `∘` := compose
+
-  postfix `⁻¹` := inverse
+  section
+
+  definition objects [coercion] (C : Category) : Type
+  := Category.rec (fun c s, c) C
+
+  definition category_instance [instance] (C : Category) : category (objects C)
+  := Category.rec (fun c s, s) C
+
+  end
 
   section
   open unit
@@ -192,19 +204,24 @@ namespace category
   parameter {ob : Type}
   definition opposite (C : category ob) : category ob :=
   category.mk (λa b, mor b a) (λ a b c f g, g ∘ f) (λ a, id) (λ a b c d f g h, symm assoc)
-    (λ a b f, id_left) (λ a b f, id_right)
+    (λ a b f, id_right) (λ a b f, id_left)
   precedence `∘op` : 60
   infixr `∘op` := @compose _ (opposite _) _ _ _
 
-  parameters {C : category ob} {a b c : ob} {f : @mor ob C a b} {g : @mor ob C b c}
+  parameters {C : category ob} {a b c : ob}
 
-  theorem compose_op : f ∘op g = g ∘ f :=
+  theorem compose_op {f : @mor ob C a b} {g : mor b c} : f ∘op g = g ∘ f :=
   rfl
 
   theorem op_op {C : category ob} : opposite (opposite C) = C :=
-  rec (λ mor comp id assoc idl idr, sorry) C
+  rec (λ mor comp id assoc idl idr, rfl) C
+
   end
 
+  definition Opposite (C : Category) : Category :=
+  Category.mk (objects C) (opposite (category_instance C))
+
+
   section
   --need extensionality
   -- definition type_cat : category Type :=
@@ -217,15 +234,18 @@ end category
 open category
 
 inductive functor {obC obD : Type} (C : category obC) (D : category obD) : Type :=
-mk : Π (obF : obC → obD) (morF : Π{A B : obC}, mor A B → mor (obF A) (obF B)),
+mk : Π (obF : obC → obD) (morF : Π⦃A B : obC⦄, mor A B → mor (obF A) (obF B)),
-    (Π {A : obC}, morF (ID A) = ID (obF A)) →
+    (Π ⦃A : obC⦄, morF (ID A) = ID (obF A)) →
-    (Π {A B C : obC} {f : mor A B} {g : mor B C}, morF (g ∘ f) = morF g ∘ morF f) →
+    (Π ⦃A B C : obC⦄ {f : mor A B} {g : mor B C}, morF (g ∘ f) = morF g ∘ morF f) →
-     @functor obC obD C D
+     functor C D
+
+inductive Functor (C D : Category) : Type :=
+mk : functor (category_instance C) (category_instance D) → Functor C D
 
 infixl `⇒`:25 := functor
 
 namespace functor
-  section
+  section basic_functor
   parameters {obC obD : Type} {C : category obC} {D : category obD}
   definition object [coercion] (F : C ⇒ D) : obC → obD := rec (λ obF morF Hid Hcomp, obF) F
 
@@ -238,10 +258,12 @@ namespace functor
   theorem respect_comp (F : C ⇒ D) : Π {a b c : obC} {f : mor a b} {g : mor b c},
       F (g ∘ f) = F g ∘ F f :=
   rec (λ obF morF Hid Hcomp, Hcomp) F
-  end
+  end basic_functor
+
+  section category_functor
 
   definition compose {obC obD obE : Type} {C : category obC} {D : category obD} {E : category obE}
-      (F : C ⇒ D) (G : D ⇒ E) : C ⇒ E :=
+      (G : D ⇒ E) (F : C ⇒ D) : C ⇒ E :=
   functor.mk C E
     (λx, G (F x))
     (λ a b f, G (F f))
@@ -252,4 +274,178 @@ namespace functor
       G (F (g ∘ f)) = G (F g ∘ F f)     : {respect_comp F}
                 ... = G (F g) ∘ G (F f) : respect_comp G)
 
+  precedence `∘∘` : 60
+  infixr `∘∘` := compose
+
+  -- theorem congr_functor {obC obD : Type} {C : category obC} {D : category obD} {o : obC → obD}
+  --     {m m' : Π⦃A B : obC⦄, mor A B → mor (o A) (o B)} {i i' c c'}
+  --     (Hm : ∀{a b : obC} {f : mor a b}, m f = m' f)
+  --       : functor.mk C D o m i c = functor.mk C D o m' i' c' :=
+  -- sorry
+
+  -- theorem congr_functor_refl {obC obD : Type} {C : category obC} {D : category obD} {o : obC → obD}
+  --     {m : Π⦃A B : obC⦄, mor A B → mor (o A) (o B)} {i i' c c'}
+  --       : functor.mk C D o m i c = functor.mk C D o m i' c' :=
+  -- rfl
+
+  theorem assoc {obA obB obC obD : Type} {A : category obA} {B : category obB}
+      {C : category obC} {D : category obD} (H : C ⇒ D) (G : B ⇒ C) (F : A ⇒ B) :
+      H ∘∘ (G ∘∘ F) = (H ∘∘ G) ∘∘ F :=
+  rfl
+
+  -- later check whether we want implicit or explicit arguments here. For the moment, define both
+  definition id {ob : Type} {C : category ob} : functor C C :=
+  mk C C (λa, a) (λ a b f, f) (λ a, rfl) (λ a b c f g, rfl)
+  definition ID {ob : Type} (C : category ob) : functor C C := id
+  definition Id {C : Category} : Functor C C := Functor.mk id
+  definition iD (C : Category) : Functor C C := Functor.mk id
+
+  theorem id_left {obC obB : Type} {B : category obB} {C : category obC} (F : B ⇒ C)
+      : id ∘∘ F = F :=
+  rec (λ obF morF idF compF, rfl) F
+
+  theorem id_right {obC obB : Type} {B : category obB} {C : category obC} (F : B ⇒ C)
+      : F ∘∘ id = F :=
+  rec (λ obF morF idF compF, rfl) F
+
+  end category_functor
+
+  section Functor
+--  parameters {C D E : Category} (G : Functor D E) (F : Functor C D)
+  definition Functor_functor {C D : Category} (F : Functor C D) : functor (category_instance C) (category_instance D) :=
+  Functor.rec (λ x, x) F
+
+  definition Compose {C D E : Category} (G : Functor D E) (F : Functor C D) : Functor C E :=
+  Functor.mk (compose (Functor_functor G) (Functor_functor F))
+
+--  namespace Functor
+  precedence `∘∘` : 60
+  infixr `∘∘` := Compose
+--  end Functor
+
+  definition Assoc {A B C D : Category} (H : Functor C D) (G : Functor B C) (F : Functor A B)
+    :  H ∘∘ (G ∘∘ F) = (H ∘∘ G) ∘∘ F :=
+  rfl
+
+  theorem Id_left {B : Category} {C : Category} (F : Functor B C)
+      : Id ∘∘ F = F :=
+  Functor.rec (λ f, subst (id_left f) rfl) F
+
+  theorem Id_right {B : Category} {C : Category} (F : Functor B C)
+      : F ∘∘ Id = F :=
+  Functor.rec (λ f, subst (id_right f) rfl) F
+
+  end Functor
+
 end functor
+
+open functor
+
+inductive natural_transformation {obC obD : Type} {C : category obC} {D : category obD}
+    (F G : functor C D) : Type :=
+mk : Π (η : Π(a : obC), mor (object F a) (object G a)), Π{a b : obC} (f : mor a b), morphism G f ∘ η a = η b ∘ morphism F f
+ → natural_transformation F G
+
+inductive Natural_transformation {C D : Category} (F G : Functor C D) : Type :=
+mk : natural_transformation (Functor_functor F) (Functor_functor G) → Natural_transformation F G
+
+namespace natural_tranformation
+
+  -- todo
+
+end natural_tranformation
+
+open functor
+namespace category
+  section cat_Cat
+
+  definition Cat : category Category :=
+  mk (λ a b, Functor a b) (λ a b c g f, Compose g f) (λ a, Id)
+     (λ a b c d h g f, Assoc h g f) (λ a b f, Id_left f) (λ a b f, Id_right f)
+
+  end cat_Cat
+
+  section slice
+  open sigma
+
+  definition slice {ob : Type} (C : category ob) (c : ob) : category (Σ(b : ob), mor b c) :=
+  mk (λa b, Σ(g : mor (dpr1 a) (dpr1 b)), dpr2 b ∘ g = dpr2 a)
+     (λ a b c g f, dpair (dpr1 g ∘ dpr1 f)
+       (calc
+         dpr2 c ∘ (dpr1 g ∘ dpr1 f) = (dpr2 c ∘ dpr1 g) ∘ dpr1 f : assoc
+           ... = dpr2 b ∘ dpr1 f : {dpr2 g}
+           ... = dpr2 a : {dpr2 f}))
+     (λ a, dpair id id_right)
+     (λ a b c d h g f, dpair_eq    assoc    proof_irrel)
+     (λ a b f,         sigma.equal id_left  proof_irrel)
+     (λ a b f,         sigma.equal id_right proof_irrel)
+  --replacing proof_irrel with rfl confuses the unifier
+  end slice
+
+
+  section coslice
+  open sigma
+
+  definition coslice {ob : Type} (C : category ob) (c : ob) : category (Σ(b : ob), mor c b) :=
+  mk (λa b, Σ(g : mor (dpr1 a) (dpr1 b)), g ∘ dpr2 a = dpr2 b)
+     (λ a b c g f, dpair (dpr1 g ∘ dpr1 f)
+       (calc
+         (dpr1 g ∘ dpr1 f) ∘ dpr2 a = dpr1 g ∘ (dpr1 f ∘ dpr2 a): symm assoc
+           ... = dpr1 g ∘ dpr2 b : {dpr2 f}
+           ... = dpr2 c : {dpr2 g}))
+     (λ a, dpair id id_left)
+     (λ a b c d h g f, dpair_eq    assoc    proof_irrel)
+     (λ a b f,         sigma.equal id_left  proof_irrel)
+     (λ a b f,         sigma.equal id_right proof_irrel)
+
+  -- theorem slice_coslice_opp {ob : Type} (C : category ob) (c : ob) :
+  --     coslice C c = opposite (slice (opposite C) c) :=
+  -- sorry
+  end coslice
+
+  section product
+  open prod
+  definition product {obC obD : Type} (C : category obC) (D : category obD)
+      : category (obC × obD) :=
+  mk (λa b, mor (pr1 a) (pr1 b) × mor (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)
+
+  end product
+
+  section arrow
+  open sigma eq_ops
+
+  definition arrow {ob : Type} (C : category ob) : category (Σ(a b : ob), mor a b) :=
+  mk (λa b, Σ(g : mor (dpr1 a) (dpr1 b)) (h : mor (dpr2' a) (dpr2' b)),
+       dpr3 b ∘ g = h ∘ dpr3 a)
+     (λ a b c g f, dpair (dpr1 g ∘ dpr1 f) (dpair (dpr2' g ∘ dpr2' f)
+       (calc
+         dpr3 c ∘ (dpr1 g ∘ dpr1 f) = (dpr3 c ∘ dpr1 g) ∘ dpr1 f : assoc
+           ... = (dpr2' g ∘ dpr3 b) ∘ dpr1 f : {dpr3 g}
+           ... = dpr2' g ∘ (dpr3 b ∘ dpr1 f) : symm assoc
+           ... = dpr2' g ∘ (dpr2' f ∘ dpr3 a) : {dpr3 f}
+           ... = (dpr2' g ∘ dpr2' f) ∘ dpr3 a : assoc)))
+     (λ a, dpair id (dpair id (id_right ⬝ (symm id_left))))
+     (λ a b c d h g f, dtrip_eq2   assoc    assoc    proof_irrel)
+     (λ a b f,         trip.equal2 id_left  id_left  proof_irrel)
+     (λ a b f,         trip.equal2 id_right id_right proof_irrel)
+     -- (λ a b c d h g f, dpair_eq assoc sorry)
+     -- (λ a b f,         sigma.equal id_left sorry)
+     -- (λ a b f,         sigma.equal id_right sorry)
+  end arrow
+
+
+  -- definition foo {obC obD : Type} (C : category obC) (D : category obD)
+  --     : category (obC × obD) :=
+  -- mk (λa b, sorry)
+  --    (λ a b c g f, sorry)
+  --    (λ a, sorry)
+  --    (λ a b c d h g f, sorry)
+  --    (λ a b f, sorry)
+  --    (λ a b f, sorry)
+
+end category

library/data/sigma.lean

@@ -27,19 +27,59 @@ section
 
   theorem dpair_eq {a₁ a₂ : A} {b₁ : B a₁} {b₂ : B a₂} (H₁ : a₁ = a₂) (H₂ : eq.rec_on H₁ b₁ = b₂) :
     dpair a₁ b₁ = dpair a₂ b₂ :=
-  eq.rec_on H₁
+  congr_arg2 dpair H₁ H₂
-    (λ (b₂ : B a₁) (H₁ : a₁ = a₁) (H₂ : eq.rec_on H₁ b₁ = b₂),
-      calc
-        dpair a₁ b₁ = dpair a₁ (eq.rec_on H₁ b₁) : {(eq.rec_on_id H₁ b₁)⁻¹}
-                ... = dpair a₁ b₂                : {H₂})
-    b₂ H₁ H₂
 
   protected theorem equal {p₁ p₂ : Σx : A, B x} :
-    ∀(H₁ : dpr1 p₁ = dpr1 p₂) (H₂ : eq.rec_on H₁ (dpr2 p₁) = (dpr2 p₂)), p₁ = p₂ :=
+    ∀(H₁ : dpr1 p₁ = dpr1 p₂) (H₂ : eq.rec_on H₁ (dpr2 p₁) = dpr2 p₂), p₁ = p₂ :=
   destruct p₁ (take a₁ b₁, destruct p₂ (take a₂ b₂ H₁ H₂, dpair_eq H₁ H₂))
 
   protected theorem is_inhabited [instance] (H₁ : inhabited A) (H₂ : inhabited (B (default A))) :
     inhabited (sigma B) :=
   inhabited.destruct H₁ (λa, inhabited.destruct H₂ (λb, inhabited.mk (dpair (default A) b)))
 end
+
+section trip_quad
+  parameters {A : Type} {B : A → Type} {C : Πa, B a → Type} {D : Πa b, C a b → Type}
+
+  definition dtrip (a : A) (b : B a) (c : C a b) := dpair a (dpair b c)
+  definition dquad (a : A) (b : B a) (c : C a b) (d : D a b c) := dpair a (dpair b (dpair c d))
+
+  definition dpr1' (x : Σ a, B a) := dpr1 x
+  definition dpr2' (x : Σ a b, C a b) := dpr1 (dpr2 x)
+  definition dpr3  (x : Σ a b, C a b) := dpr2 (dpr2 x)
+  definition dpr3' (x : Σ a b c, D a b c) := dpr1 (dpr2 (dpr2 x))
+  definition dpr4  (x : Σ a b c, D a b c) := dpr2 (dpr2 (dpr2 x))
+
+  -- theorem dtrip_eq {a₁ a₂ : A} {b₁ : B a₁} {b₂ : B a₂} {c₁ : C a₁ b₁} {c₂ : C a₂ b₂}
+  --     (H₁ : a₁ = a₂)  (H₂ : eq.rec_on H₁ b₁ = b₂) (H₃ : eq.rec_on (congr_arg2 C H₁ H₂) c₁ = c₂) :
+  --   dtrip a₁ b₁ c₁ = dtrip a₂ b₂ c₂ :=
+  -- eq.rec_on H₁
+  --   (λ (b₂ : B a₁) (c₂ : C a₁ b₂) (H₁ : a₁ = a₁) (H₂ : eq.rec_on H₁ b₁ = b₂)
+  --       (x : (eq (eq.rec_on (congr_arg2 C H₁ H₂) c₁) c₂)), sorry
+  --     -- have H : dpair b₁ c₁ = dpair b₂ c₂, from
+  --     --   dpair_eq H₂ (eq.subst (eq.rec_on_id H₁ c₁) H₃),
+  --     -- eq.subst H rfl
+  --   )
+  --   b₂ c₂ H₁ H₂ H₃
+end trip_quad
+
+  theorem dtrip_eq2 {A B : Type} {C : A → B → Type} {a₁ a₂ : A} {b₁ b₂ : B}
+      {c₁ : C a₁ b₁} {c₂ : C a₂ b₂} (H₁ : a₁ = a₂)  (H₂ : b₁ = b₂)
+      (H₃ : eq.rec_on H₂ (eq.rec_on H₁ c₁) = c₂) :
+    dtrip a₁ b₁ c₁ = dtrip a₂ b₂ c₂ :=
+  eq.rec_on H₁
+    (λ (b₂ : B) (c₂ : C a₁ b₂) (H₁ : a₁ = a₁) (H₂ : b₁ = b₂)
+        (H₃ : eq.rec_on H₂ (eq.rec_on H₁ c₁) = c₂),
+      have H : dpair b₁ c₁ = dpair b₂ c₂, from
+        dpair_eq H₂ (eq.subst (eq.rec_on_id H₁ c₁) H₃),
+      eq.subst H rfl
+    )
+    b₂ c₂ H₁ H₂ H₃
+
+  theorem trip.equal2 {A B : Type} {C : A → B → Type} {p₁ p₂ : Σa b, C a b} :
+      ∀(H₁ : dpr1 p₁ = dpr1 p₂) (H₂ : dpr2' p₁ = dpr2' p₂)
+      (H₃ : eq.rec_on H₂ (eq.rec_on H₁ (dpr3 p₁)) = dpr3 p₂), p₁ = p₂ :=
+  destruct p₁ (take a₁ q₁, destruct q₁ (take b₁ c₁, destruct p₂ (take a₂ q₂, destruct q₂
+    (take b₂ c₂ H₁ H₂ H₃, dtrip_eq2 H₁ H₂ H₃))))
+
 end sigma

library/hott/path.lean

@@ -40,9 +40,9 @@ infixl `@`:75 := concat
 postfix `^`:100 := inverse
 
 -- In Coq, these are not needed, because concat and inv are kept transparent
-definition inv_1 {A : Type} (x : A) : (idpath x)^ ≈ idpath x := idp
+-- definition inv_1 {A : Type} (x : A) : (idpath x)^ ≈ idpath x := idp
 
-definition concat_11 {A : Type} (x : A) : idpath x @ idpath x ≈ idpath x := idp
+-- definition concat_11 {A : Type} (x : A) : idpath x @ idpath x ≈ idpath x := idp
 
 
 -- The 1-dimensional groupoid structure

library/logic/core/eq.lean

@@ -71,6 +71,16 @@ H ▸ rfl
 theorem congr_arg {A : Type} {B : Type} {a b : A} (f : A → B) (H : a = b) : f a = f b :=
 H ▸ rfl
 
+theorem congr_arg2 {A : Type} {B : A → Type} {C : Type} {a₁ a₂ : A}
+    {b₁ : B a₁} {b₂ : B a₂} (f : Πa, B a → C) (H₁ : a₁ = a₂) (H₂ : eq.rec_on H₁ b₁ = b₂) :
+    f a₁ b₁ = f a₂ b₂ :=
+  eq.rec_on H₁
+    (λ (b₂ : B a₁) (H₁ : a₁ = a₁) (H₂ : eq.rec_on H₁ b₁ = b₂),
+      calc
+        f a₁ b₁ = f a₁ (eq.rec_on H₁ b₁) : {(eq.rec_on_id H₁ b₁)⁻¹}
+            ... = f a₁ b₂                : {H₂})
+    b₂ H₁ H₂
+
 theorem congr {A : Type} {B : Type} {f g : A → B} {a b : A} (H1 : f = g) (H2 : a = b) :
   f a = g b :=
 H1 ▸ H2 ▸ rfl
@@ -99,6 +109,9 @@ assume Ha, H2 ▸ (H1 Ha)
 theorem eq_imp_trans {a b c : Prop} (H1 : a = b) (H2 : b → c) : a → c :=
 assume Ha, H2 (H1 ▸ Ha)
 
+-- proof irrelevance is built in the kernel
+theorem proof_irrel {a : Prop} {H1 H2 : a} : H1 = H2 := rfl
+
 -- ne
 -- --