From 8c5d3392c771ee0717bebe064415d2a925d211ff Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 8 Oct 2014 23:44:09 -0700 Subject: [PATCH] fix(library/algebra/category): minor fixes to reflect recent changes, and fix tests --- library/algebra/category/adjoint.lean | 13 +- library/algebra/category/constructions.lean | 86 ++++---- tests/lean/bad_class.lean | 3 +- tests/lean/bad_class.lean.expected.out | 2 +- tests/lean/run/coe11.lean | 18 +- tests/lean/run/mor.lean | 6 +- tests/lean/run/print.lean | 2 +- tests/lean/slow/cat_sec_var_bug.lean | 215 -------------------- 8 files changed, 67 insertions(+), 278 deletions(-) diff --git a/library/algebra/category/adjoint.lean b/library/algebra/category/adjoint.lean index ac413450b..5cb400df5 100644 --- a/library/algebra/category/adjoint.lean +++ b/library/algebra/category/adjoint.lean @@ -13,18 +13,21 @@ namespace adjoint definition Hom {obC : Type} (C : category obC) : 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, + (λ 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 section parameters {obC obD : Type} (C : category obC) {D : category obD} - definition adjoint (F : C ⇒ D) (G : D ⇒ C) := + -- Add auxiliary category instance needed by functor.compose at (Hom D ∘f sorry) + private definition aux_prod_cat [instance] : category (obD × obD) := prod_category (opposite.opposite D) D + + definition adjoint (obC obD : Type) (C : category obC) (D : category obD) (F : C ⇒ D) (G : D ⇒ C) := natural_transformation (Hom D ∘f sorry) - --(Hom C ∘f sorry) + --(Hom C ∘f sorry) --product.prod_functor (opposite.opposite_functor F) (functor.ID D) end diff --git a/library/algebra/category/constructions.lean b/library/algebra/category/constructions.lean index 3312013ba..d8c68f222 100644 --- a/library/algebra/category/constructions.lean +++ b/library/algebra/category/constructions.lean @@ -115,7 +115,7 @@ namespace ops notation 1 := category_one postfix `ᵒᵖ`:max := opposite.opposite infixr `×c`:30 := product.prod_category - instance category_of_categories type_category category_one product.prod_category + instance [persistent] category_of_categories type_category category_one product.prod_category end ops open ops namespace opposite @@ -125,10 +125,10 @@ end ops definition opposite_functor {obC obD : Type} {C : category obC} {D : category obD} (F : C ⇒ D) : Cᵒᵖ ⇒ Dᵒᵖ := @functor.mk obC obD (Cᵒᵖ) (Dᵒᵖ) - (λ a, F a) - (λ a b f, F f) - (λ a, !respect_id) - (λ a b c g f, !respect_comp) + (λ a, F a) + (λ a b f, F f) + (λ a, !respect_id) + (λ a b c g f, !respect_comp) end end opposite @@ -138,9 +138,9 @@ end ops definition prod_functor {obC obC' obD obD' : Type} {C : category obC} {C' : category obC'} {D : category obD} {D' : category obD'} (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) - (λ a b c g f, pair_eq !respect_comp !respect_comp) + (λ a b f, pair (F (pr1 f)) (G (pr2 f))) + (λ a, pair_eq !respect_id !respect_id) + (λ a b c g f, pair_eq !respect_comp !respect_comp) end end product @@ -167,12 +167,12 @@ end ops mk (λa b, Σ(g : hom (dpr1 a) (dpr1 b)), dpr2 b ∘ g = dpr2 a) (λ a b c g f, dpair (dpr1 g ∘ dpr1 f) (show dpr2 c ∘ (dpr1 g ∘ dpr1 f) = dpr2 a, - proof - calc - dpr2 c ∘ (dpr1 g ∘ dpr1 f) = (dpr2 c ∘ dpr1 g) ∘ dpr1 f : !assoc - ... = dpr2 b ∘ dpr1 f : {dpr2 g} - ... = dpr2 a : {dpr2 f} - qed)) + proof + calc + dpr2 c ∘ (dpr1 g ∘ dpr1 f) = (dpr2 c ∘ dpr1 g) ∘ dpr1 f : !assoc + ... = dpr2 b ∘ dpr1 f : {dpr2 g} + ... = dpr2 a : {dpr2 f} + qed)) (λ 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) @@ -182,31 +182,31 @@ end ops namespace slice section --remove open sigma category.ops --remove sigma - instance slice_category + instance [persistent] slice_category parameters {ob : Type} (C : category ob) definition forgetful (x : ob) : (slice_category C x) ⇒ C := functor.mk (λ a, dpr1 a) - (λ a b f, dpr1 f) - (λ a, rfl) - (λ a b c g f, rfl) + (λ a b f, dpr1 f) + (λ a, rfl) + (λ a b c g f, rfl) definition composition_functor {x y : ob} (h : x ⟶ y) : slice_category C x ⇒ slice_category C y := functor.mk (λ a, dpair (dpr1 a) (h ∘ dpr2 a)) - (λ a b f, dpair (dpr1 f) - (calc - (h ∘ dpr2 b) ∘ dpr1 f = h ∘ (dpr2 b ∘ dpr1 f) : !assoc⁻¹ - ... = h ∘ dpr2 a : {dpr2 f})) - (λ a, rfl) - (λ a b c g f, dpair_eq rfl !proof_irrel) + (λ a b f, dpair (dpr1 f) + (calc + (h ∘ dpr2 b) ∘ dpr1 f = h ∘ (dpr2 b ∘ dpr1 f) : !assoc⁻¹ + ... = h ∘ dpr2 a : {dpr2 f})) + (λ a, rfl) + (λ a b c g f, dpair_eq rfl !proof_irrel) -- the following definition becomes complicated -- definition slice_functor : C ⇒ category_of_categories := -- functor.mk (λ a, Category.mk _ (slice_category C a)) -- (λ a b f, Functor.mk (composition_functor f)) -- (λ a, congr_arg Functor.mk -- (congr_arg4_dep functor.mk - -- (funext (λx, sigma.equal rfl !id_left)) - -- sorry - -- !proof_irrel - -- !proof_irrel)) + -- (funext (λx, sigma.equal rfl !id_left)) + -- sorry + -- !proof_irrel + -- !proof_irrel)) -- (λ a b c g f, sorry) end end slice @@ -218,12 +218,12 @@ end ops mk (λa b, Σ(g : hom (dpr1 a) (dpr1 b)), g ∘ dpr2 a = dpr2 b) (λ a b c g f, dpair (dpr1 g ∘ dpr1 f) (show (dpr1 g ∘ dpr1 f) ∘ dpr2 a = dpr2 c, - proof - 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} - qed)) + proof + 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} + qed)) (λ 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) @@ -275,15 +275,15 @@ end ops definition arrow (ob : Type) (C : category ob) : category (arrow_obs ob C) := mk (λa b, arrow_hom a b) (λ a b c g f, dpair (hom_src g ∘ hom_src f) (dpair (hom_dst g ∘ hom_dst f) - (show to_hom c ∘ (hom_src g ∘ hom_src f) = (hom_dst g ∘ hom_dst f) ∘ to_hom a, - proof - calc - to_hom c ∘ (hom_src g ∘ hom_src f) = (to_hom c ∘ hom_src g) ∘ hom_src f : !assoc - ... = (hom_dst g ∘ to_hom b) ∘ hom_src f : {commute g} - ... = hom_dst g ∘ (to_hom b ∘ hom_src f) : symm !assoc - ... = hom_dst g ∘ (hom_dst f ∘ to_hom a) : {commute f} - ... = (hom_dst g ∘ hom_dst f) ∘ to_hom a : !assoc - qed) + (show to_hom c ∘ (hom_src g ∘ hom_src f) = (hom_dst g ∘ hom_dst f) ∘ to_hom a, + proof + calc + to_hom c ∘ (hom_src g ∘ hom_src f) = (to_hom c ∘ hom_src g) ∘ hom_src f : !assoc + ... = (hom_dst g ∘ to_hom b) ∘ hom_src f : {commute g} + ... = hom_dst g ∘ (to_hom b ∘ hom_src f) : symm !assoc + ... = hom_dst g ∘ (hom_dst f ∘ to_hom a) : {commute f} + ... = (hom_dst g ∘ hom_dst f) ∘ to_hom a : !assoc + qed) )) (λ a, dpair id (dpair id (!id_right ⬝ (symm !id_left)))) (λ a b c d h g f, dtrip_eq_ndep !assoc !assoc !proof_irrel) diff --git a/tests/lean/bad_class.lean b/tests/lean/bad_class.lean index df38cfa1d..5668cf64f 100644 --- a/tests/lean/bad_class.lean +++ b/tests/lean/bad_class.lean @@ -1,7 +1,8 @@ import logic - +namespace foo definition subsingleton (A : Type) := ∀⦃a b : A⦄, a = b class subsingleton protected definition prop.subsingleton [instance] (P : Prop) : subsingleton P := λa b, !proof_irrel +end foo diff --git a/tests/lean/bad_class.lean.expected.out b/tests/lean/bad_class.lean.expected.out index 4fe2501b9..7c8f87591 100644 --- a/tests/lean/bad_class.lean.expected.out +++ b/tests/lean/bad_class.lean.expected.out @@ -1,2 +1,2 @@ -bad_class.lean:4:0: error: invalid class, 'subsingleton' is a definition +bad_class.lean:4:0: error: invalid class, 'foo.subsingleton' is a definition bad_class.lean:6:0: error: 'eq' is not a class diff --git a/tests/lean/run/coe11.lean b/tests/lean/run/coe11.lean index 72e8fe87c..095b41d7c 100644 --- a/tests/lean/run/coe11.lean +++ b/tests/lean/run/coe11.lean @@ -1,18 +1,18 @@ -import algebra.category +import algebra.category.basic open category inductive my_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)), - (Π {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) → +mk : Π (obF : obC → obD) (homF : Π{A B : obC}, hom A B → hom (obF A) (obF B)), + (Π {A : obC}, homF (ID A) = ID (obF A)) → + (Π {A B C : obC} {f : hom A B} {g : hom B C}, homF (g ∘ f) = homF g ∘ homF f) → my_functor C D definition my_object [coercion] {obC obD : Type} {C : category obC} {D : category obD} (F : my_functor C D) : obC → obD := -my_functor.rec (λ obF morF Hid Hcomp, obF) F +my_functor.rec (λ obF homF Hid Hcomp, obF) F -definition my_morphism [coercion] {obC obD : Type} {C : category obC} {D : category obD} (F : my_functor C D) : - Π{A B : obC}, mor A B → mor (my_object F A) (my_object F B) := -my_functor.rec (λ obF morF Hid Hcomp, morF) F +definition my_homphism [coercion] {obC obD : Type} {C : category obC} {D : category obD} (F : my_functor C D) : + Π{A B : obC}, hom A B → hom (my_object F A) (my_object F B) := +my_functor.rec (λ obF homF Hid Hcomp, homF) F constants obC obD : Type constants a b : obC @@ -20,6 +20,6 @@ constant C : category obC instance C constant D : category obD constant F : my_functor C D -constant m : mor a b +constant m : hom a b check F a check F m diff --git a/tests/lean/run/mor.lean b/tests/lean/run/mor.lean index 126a492ad..4f3998598 100644 --- a/tests/lean/run/mor.lean +++ b/tests/lean/run/mor.lean @@ -2,7 +2,7 @@ -- Released under Apache 2.0 license as described in the file LICENSE. -- Author: Floris van Doorn -import algebra.category +import algebra.category.basic open eq eq.ops category @@ -10,7 +10,7 @@ namespace morphism section parameter {ob : Type} parameter {C : category ob} - variables {a b c d : ob} {h : mor c d} {g : mor b c} {f : mor a b} - check mor a b + variables {a b c d : ob} {h : hom c d} {g : hom b c} {f : hom a b} + check hom a b end end morphism diff --git a/tests/lean/run/print.lean b/tests/lean/run/print.lean index de0892c7c..b6af55c7b 100644 --- a/tests/lean/run/print.lean +++ b/tests/lean/run/print.lean @@ -1,4 +1,4 @@ -import data.num logic data.prod data.nat data.int algebra.category +import data.num logic data.prod data.nat data.int algebra.category.basic open num prod int nat category functor print instances inhabited diff --git a/tests/lean/slow/cat_sec_var_bug.lean b/tests/lean/slow/cat_sec_var_bug.lean index 01c597adb..b05f01f8f 100644 --- a/tests/lean/slow/cat_sec_var_bug.lean +++ b/tests/lean/slow/cat_sec_var_bug.lean @@ -314,219 +314,4 @@ namespace natural_transformation end precedence `∘n` : 60 infixr `∘n` := compose - section - variables {obC obD : Type} {C : category obC} {D : category obD} {F₁ F₂ F₃ F₄ : C ⇒ D} - protected theorem assoc (η₃ : F₃ ==> F₄) (η₂ : F₂ ==> F₃) (η₁ : F₁ ==> F₂) : - η₃ ∘n (η₂ ∘n η₁) = (η₃ ∘n η₂) ∘n η₁ := - congr_arg2_dep mk (funext (take x, !assoc)) proof_irrel - - --TODO: check whether some of the below identities are superfluous - protected definition id {obC obD : Type} {C : category obC} {D : category obD} {F : C ⇒ D} - : natural_transformation F F := - mk (λa, id) (λa b f, !id_right ⬝ symm !id_left) - protected definition ID {obC obD : Type} {C : category obC} {D : category obD} (F : C ⇒ D) - : natural_transformation F F := id - -- protected definition Id {C D : Category} {F : Functor C D} : Natural_transformation F F := - -- Natural_transformation.mk id - -- protected definition iD {C D : Category} (F : Functor C D) : Natural_transformation F F := - -- Natural_transformation.mk id - - protected theorem id_left (η : F₁ ==> F₂) : natural_transformation.compose id η = η := - rec (λf H, congr_arg2_dep mk (funext (take x, !id_left)) proof_irrel) η - - protected theorem id_right (η : F₁ ==> F₂) : natural_transformation.compose η id = η := - rec (λf H, congr_arg2_dep mk (funext (take x, !id_right)) proof_irrel) η - - end end natural_transformation - --- examples of categories / basic constructions (TODO: move to separate file) - -open functor -namespace category - section - open unit - definition one [instance] : category unit := - category.mk (λa b, unit) (λ a b c f g, star) (λ a, star) (λ a b c d f g h, unit.equal _ _) - (λ a b f, unit.equal _ _) (λ a b f, unit.equal _ _) - end - - section - open unit - definition big_one_test (A : Type) : category A := - category.mk (λa b, unit) (λ a b c f g, star) (λ a, star) (λ a b c d f g h, unit.equal _ _) - (λ a b f, unit.equal _ _) (λ a b f, unit.equal _ _) - end - - section - parameter {ob : Type} - definition opposite (C : category ob) : category ob := - category.mk (λa b, hom b a) (λ a b c f g, g ∘ f) (λ a, id) (λ a b c d f g h, symm !assoc) - (λ 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} - - theorem compose_op {f : @hom ob C a b} {g : hom b c} : f ∘op g = g ∘ f := - rfl - - theorem op_op {C : category ob} : opposite (opposite C) = C := - category.rec (λ hom comp id assoc idl idr, refl (mk _ _ _ _ _ _)) C - end - - definition Opposite (C : Category) : Category := - Category.mk (objects C) (opposite (category_instance C)) - - - section - definition type_category : category Type := - mk (λA B, A → B) (λ a b c, function.compose) (λ a, function.id) - (λ a b c d h g f, symm (function.compose_assoc h g f)) - (λ a b f, function.compose_id_left f) (λ a b f, function.compose_id_right f) - end - - section cat_C - - definition C : category Category := - mk (λ a b, Functor a b) (λ a b c g f, functor.Compose g f) (λ a, functor.Id) - (λ a b c d h g f, !functor.Assoc) (λ a b f, !functor.Id_left) - (λ a b f, !functor.Id_right) - - end cat_C - - section functor_category - parameters {obC obD : Type} (C : category obC) (D : category obD) - definition functor_category : category (functor C D) := - mk (λa b, natural_transformation a b) - (λ a b c g f, natural_transformation.compose g f) - (λ a, natural_transformation.id) - (λ a b c d h g f, !natural_transformation.assoc) - (λ a b f, !natural_transformation.id_left) - (λ a b f, !natural_transformation.id_right) - end functor_category - - - section slice - open sigma - - definition slice {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) - (show dpr2 c ∘ (dpr1 g ∘ dpr1 f) = dpr2 a, - proof - calc - dpr2 c ∘ (dpr1 g ∘ dpr1 f) = (dpr2 c ∘ dpr1 g) ∘ dpr1 f : !assoc - ... = dpr2 b ∘ dpr1 f : {dpr2 g} - ... = dpr2 a : {dpr2 f} - qed)) - (λ 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) - -- We give proof_irrel instead of rfl, to give the unifier an easier time - end slice - - section coslice - open sigma - - definition coslice {ob : Type} (C : category ob) (c : ob) : category (Σ(b : ob), hom c b) := - mk (λa b, Σ(g : hom (dpr1 a) (dpr1 b)), g ∘ dpr2 a = dpr2 b) - (λ a b c g f, dpair (dpr1 g ∘ dpr1 f) - (show (dpr1 g ∘ dpr1 f) ∘ dpr2 a = dpr2 c, - proof - 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} - qed)) - (λ 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, 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) - - end product - - section arrow - open sigma eq.ops - -- theorem concat_commutative_squares {ob : Type} {C : category ob} {a1 a2 a3 b1 b2 b3 : ob} - -- {f1 : a1 => b1} {f2 : a2 => b2} {f3 : a3 => b3} {g2 : a2 => a3} {g1 : a1 => a2} - -- {h2 : b2 => b3} {h1 : b1 => b2} (H1 : f2 ∘ g1 = h1 ∘ f1) (H2 : f3 ∘ g2 = h2 ∘ f2) - -- : f3 ∘ (g2 ∘ g1) = (h2 ∘ h1) ∘ f1 := - -- calc - -- f3 ∘ (g2 ∘ g1) = (f3 ∘ g2) ∘ g1 : assoc - -- ... = (h2 ∘ f2) ∘ g1 : {H2} - -- ... = h2 ∘ (f2 ∘ g1) : symm assoc - -- ... = h2 ∘ (h1 ∘ f1) : {H1} - -- ... = (h2 ∘ h1) ∘ f1 : assoc - - -- definition arrow {ob : Type} (C : category ob) : category (Σ(a b : ob), hom a b) := - -- mk (λa b, Σ(g : hom (dpr1 a) (dpr1 b)) (h : hom (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) (concat_commutative_squares (dpr3 f) (dpr3 g)))) - -- (λ 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) - - variables {ob : Type} {C : category ob} - protected definition arrow_obs (ob : Type) (C : category ob) := Σ(a b : ob), hom a b - variables {a b : arrow_obs ob C} - protected definition src (a : arrow_obs ob C) : ob := dpr1 a - protected definition dst (a : arrow_obs ob C) : ob := dpr2' a - protected definition to_hom (a : arrow_obs ob C) : hom (src a) (dst a) := dpr3 a - - protected definition arrow_hom (a b : arrow_obs ob C) : Type := - Σ (g : hom (src a) (src b)) (h : hom (dst a) (dst b)), to_hom b ∘ g = h ∘ to_hom a - - protected definition hom_src (m : arrow_hom a b) : hom (src a) (src b) := dpr1 m - protected definition hom_dst (m : arrow_hom a b) : hom (dst a) (dst b) := dpr2' m - protected definition commute (m : arrow_hom a b) : to_hom b ∘ (hom_src m) = (hom_dst m) ∘ to_hom a - := dpr3 m - - definition arrow (ob : Type) (C : category ob) : category (arrow_obs ob C) := - mk (λa b, arrow_hom a b) - (λ a b c g f, dpair (hom_src g ∘ hom_src f) (dpair (hom_dst g ∘ hom_dst f) - (show to_hom c ∘ (hom_src g ∘ hom_src f) = (hom_dst g ∘ hom_dst f) ∘ to_hom a, - proof - calc - to_hom c ∘ (hom_src g ∘ hom_src f) = (to_hom c ∘ hom_src g) ∘ hom_src f : !assoc - ... = (hom_dst g ∘ to_hom b) ∘ hom_src f : {commute g} - ... = hom_dst g ∘ (to_hom b ∘ hom_src f) : symm !assoc - ... = hom_dst g ∘ (hom_dst f ∘ to_hom a) : {commute f} - ... = (hom_dst g ∘ hom_dst f) ∘ to_hom a : !assoc - qed) - )) - (λ a, dpair id (dpair id (!id_right ⬝ (symm !id_left)))) - (λ a b c d h g f, dtrip_eq_ndep !assoc !assoc proof_irrel) - (λ a b f, trip.equal_ndep !id_left !id_left proof_irrel) - (λ a b f, trip.equal_ndep !id_right !id_right proof_irrel) - - end arrow - - -- definition foo - -- : category (sorry) := - -- 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