fix(library/algebra/category): minor fixes to reflect recent changes, and fix tests
This commit is contained in:
Leonardo de Moura
parent
0a58e3d1ae
commit
8c5d3392c7
8 changed files with 67 additions and 278 deletions
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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)
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
Loading…
Reference in a new issue