Members/kono/Proof/category: cat-utility.agda annotate

annotate cat-utility.agda @ 694:2043f7fd4273

Added tag current for changeset 984518c56e96

author	Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date	Mon, 13 Nov 2017 12:39:43 +0900
parents	917e51be9bbf
children	7a6ee564e3a8

rev	line source
56 83ff8d48fdca add unitility Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	1 module cat-utility where
83ff8d48fdca add unitility Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	2
83ff8d48fdca add unitility Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	3 -- Shinji KONO <kono@ie.u-ryukyu.ac.jp>
83ff8d48fdca add unitility Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	4
87 4690953794c4 MEsolution Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 86 diff changeset	5 open import Category -- https://github.com/konn/category-agda
4690953794c4 MEsolution Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 86 diff changeset	6 open import Level
4690953794c4 MEsolution Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 86 diff changeset	7 --open import Category.HomReasoning
4690953794c4 MEsolution Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 86 diff changeset	8 open import HomReasoning
56 83ff8d48fdca add unitility Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	9
87 4690953794c4 MEsolution Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 86 diff changeset	10 open Functor
56 83ff8d48fdca add unitility Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	11
87 4690953794c4 MEsolution Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 86 diff changeset	12 id1 : ∀{c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (a : Obj A ) → Hom A a a
4690953794c4 MEsolution Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 86 diff changeset	13 id1 A a = (Id {_} {_} {_} {A} a)
253 24e83b8b81be fix Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 202 diff changeset	14 -- We cannot make A implicit
56 83ff8d48fdca add unitility Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	15
468 c375d8f93a2c discrete category and product from a limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 460 diff changeset	16 record IsUniversalMapping {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ')
87 4690953794c4 MEsolution Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 86 diff changeset	17 ( U : Functor B A )
4690953794c4 MEsolution Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 86 diff changeset	18 ( F : Obj A → Obj B )
4690953794c4 MEsolution Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 86 diff changeset	19 ( η : (a : Obj A) → Hom A a ( FObj U (F a) ) )
4690953794c4 MEsolution Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 86 diff changeset	20 ( _* : { a : Obj A}{ b : Obj B} → ( Hom A a (FObj U b) ) → Hom B (F a ) b )
4690953794c4 MEsolution Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 86 diff changeset	21 : Set (suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁' ⊔ c₂' ⊔ ℓ' )) where
4690953794c4 MEsolution Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 86 diff changeset	22 field
468 c375d8f93a2c discrete category and product from a limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 460 diff changeset	23 universalMapping : {a : Obj A} { b : Obj B } → { f : Hom A a (FObj U b) } →
101 0f7086b6a1a6 on going ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 94 diff changeset	24 A [ A [ FMap U ( f * ) o η a ] ≈ f ]
468 c375d8f93a2c discrete category and product from a limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 460 diff changeset	25 uniquness : {a : Obj A} { b : Obj B } → { f : Hom A a (FObj U b) } → { g : Hom B (F a) b } →
101 0f7086b6a1a6 on going ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 94 diff changeset	26 A [ A [ FMap U g o η a ] ≈ f ] → B [ f * ≈ g ]
56 83ff8d48fdca add unitility Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	27
468 c375d8f93a2c discrete category and product from a limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 460 diff changeset	28 record UniversalMapping {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ')
689 fb9fc9652c04 fix again Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 688 diff changeset	29 ( U : Functor B A )
87 4690953794c4 MEsolution Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 86 diff changeset	30 : Set (suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁' ⊔ c₂' ⊔ ℓ' )) where
4690953794c4 MEsolution Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 86 diff changeset	31 infixr 11 _*
4690953794c4 MEsolution Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 86 diff changeset	32 field
690 3d41a8edbf63 fix universal mapping done. Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 689 diff changeset	33 F : Obj A → Obj B
3d41a8edbf63 fix universal mapping done. Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 689 diff changeset	34 η : (a : Obj A) → Hom A a ( FObj U (F a) )
468 c375d8f93a2c discrete category and product from a limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 460 diff changeset	35 _* : { a : Obj A}{ b : Obj B} → ( Hom A a (FObj U b) ) → Hom B (F a ) b
87 4690953794c4 MEsolution Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 86 diff changeset	36 isUniversalMapping : IsUniversalMapping A B U F η _*
56 83ff8d48fdca add unitility Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	37
468 c375d8f93a2c discrete category and product from a limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 460 diff changeset	38 record coIsUniversalMapping {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ')
268 2ff44ee3cb32 co universal mapping Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 265 diff changeset	39 ( F : Functor A B )
2ff44ee3cb32 co universal mapping Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 265 diff changeset	40 ( U : Obj B → Obj A )
2ff44ee3cb32 co universal mapping Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 265 diff changeset	41 ( ε : (b : Obj B) → Hom B ( FObj F (U b) ) b )
2ff44ee3cb32 co universal mapping Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 265 diff changeset	42 ( _*' : { b : Obj B}{ a : Obj A} → ( Hom B (FObj F a) b ) → Hom A a (U b ) )
2ff44ee3cb32 co universal mapping Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 265 diff changeset	43 : Set (suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁' ⊔ c₂' ⊔ ℓ' )) where
2ff44ee3cb32 co universal mapping Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 265 diff changeset	44 field
468 c375d8f93a2c discrete category and product from a limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 460 diff changeset	45 couniversalMapping : {b : Obj B} { a : Obj A } → { f : Hom B (FObj F a) b } →
268 2ff44ee3cb32 co universal mapping Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 265 diff changeset	46 B [ B [ ε b o FMap F ( f *' ) ] ≈ f ]
468 c375d8f93a2c discrete category and product from a limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 460 diff changeset	47 couniquness : {b : Obj B} { a : Obj A } → { f : Hom B (FObj F a) b } → { g : Hom A a (U b) } →
268 2ff44ee3cb32 co universal mapping Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 265 diff changeset	48 B [ B [ ε b o FMap F g ] ≈ f ] → A [ f *' ≈ g ]
2ff44ee3cb32 co universal mapping Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 265 diff changeset	49
468 c375d8f93a2c discrete category and product from a limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 460 diff changeset	50 record coUniversalMapping {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ')
689 fb9fc9652c04 fix again Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 688 diff changeset	51 ( F : Functor A B )
268 2ff44ee3cb32 co universal mapping Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 265 diff changeset	52 : Set (suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁' ⊔ c₂' ⊔ ℓ' )) where
2ff44ee3cb32 co universal mapping Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 265 diff changeset	53 infixr 11 _*'
2ff44ee3cb32 co universal mapping Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 265 diff changeset	54 field
690 3d41a8edbf63 fix universal mapping done. Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 689 diff changeset	55 U : Obj B → Obj A
3d41a8edbf63 fix universal mapping done. Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 689 diff changeset	56 ε : (b : Obj B) → Hom B ( FObj F (U b) ) b
468 c375d8f93a2c discrete category and product from a limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 460 diff changeset	57 _*' : { b : Obj B}{ a : Obj A} → ( Hom B (FObj F a) b ) → Hom A a (U b )
268 2ff44ee3cb32 co universal mapping Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 265 diff changeset	58 iscoUniversalMapping : coIsUniversalMapping A B F U ε _*'
2ff44ee3cb32 co universal mapping Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 265 diff changeset	59
87 4690953794c4 MEsolution Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 86 diff changeset	60 open NTrans
4690953794c4 MEsolution Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 86 diff changeset	61 open import Category.Cat
468 c375d8f93a2c discrete category and product from a limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 460 diff changeset	62 record IsAdjunction {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ')
87 4690953794c4 MEsolution Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 86 diff changeset	63 ( U : Functor B A )
4690953794c4 MEsolution Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 86 diff changeset	64 ( F : Functor A B )
4690953794c4 MEsolution Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 86 diff changeset	65 ( η : NTrans A A identityFunctor ( U ○ F ) )
4690953794c4 MEsolution Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 86 diff changeset	66 ( ε : NTrans B B ( F ○ U ) identityFunctor )
4690953794c4 MEsolution Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 86 diff changeset	67 : Set (suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁' ⊔ c₂' ⊔ ℓ' )) where
4690953794c4 MEsolution Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 86 diff changeset	68 field
4690953794c4 MEsolution Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 86 diff changeset	69 adjoint1 : { b : Obj B } →
4690953794c4 MEsolution Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 86 diff changeset	70 A [ A [ ( FMap U ( TMap ε b )) o ( TMap η ( FObj U b )) ] ≈ id1 A (FObj U b) ]
4690953794c4 MEsolution Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 86 diff changeset	71 adjoint2 : {a : Obj A} →
4690953794c4 MEsolution Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 86 diff changeset	72 B [ B [ ( TMap ε ( FObj F a )) o ( FMap F ( TMap η a )) ] ≈ id1 B (FObj F a) ]
56 83ff8d48fdca add unitility Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	73
468 c375d8f93a2c discrete category and product from a limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 460 diff changeset	74 record Adjunction {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ')
87 4690953794c4 MEsolution Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 86 diff changeset	75 : Set (suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁' ⊔ c₂' ⊔ ℓ' )) where
4690953794c4 MEsolution Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 86 diff changeset	76 field
688 a5f2ca67e7c5 fix monad/adjunction definition Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 681 diff changeset	77 U : Functor B A
a5f2ca67e7c5 fix monad/adjunction definition Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 681 diff changeset	78 F : Functor A B
a5f2ca67e7c5 fix monad/adjunction definition Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 681 diff changeset	79 η : NTrans A A identityFunctor ( U ○ F )
a5f2ca67e7c5 fix monad/adjunction definition Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 681 diff changeset	80 ε : NTrans B B ( F ○ U ) identityFunctor
87 4690953794c4 MEsolution Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 86 diff changeset	81 isAdjunction : IsAdjunction A B U F η ε
202 58ee98bbb333 remove an extensionality Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 176 diff changeset	82 U-functor = U
58ee98bbb333 remove an extensionality Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 176 diff changeset	83 F-functor = F
58ee98bbb333 remove an extensionality Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 176 diff changeset	84 Eta = η
58ee98bbb333 remove an extensionality Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 176 diff changeset	85 Epsiron = ε
56 83ff8d48fdca add unitility Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	86
83ff8d48fdca add unitility Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	87
468 c375d8f93a2c discrete category and product from a limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 460 diff changeset	88 record IsMonad {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ)
87 4690953794c4 MEsolution Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 86 diff changeset	89 ( T : Functor A A )
4690953794c4 MEsolution Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 86 diff changeset	90 ( η : NTrans A A identityFunctor T )
4690953794c4 MEsolution Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 86 diff changeset	91 ( μ : NTrans A A (T ○ T) T)
4690953794c4 MEsolution Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 86 diff changeset	92 : Set (suc (c₁ ⊔ c₂ ⊔ ℓ )) where
4690953794c4 MEsolution Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 86 diff changeset	93 field
4690953794c4 MEsolution Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 86 diff changeset	94 assoc : {a : Obj A} → A [ A [ TMap μ a o TMap μ ( FObj T a ) ] ≈ A [ TMap μ a o FMap T (TMap μ a) ] ]
4690953794c4 MEsolution Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 86 diff changeset	95 unity1 : {a : Obj A} → A [ A [ TMap μ a o TMap η ( FObj T a ) ] ≈ Id {_} {_} {_} {A} (FObj T a) ]
4690953794c4 MEsolution Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 86 diff changeset	96 unity2 : {a : Obj A} → A [ A [ TMap μ a o (FMap T (TMap η a ))] ≈ Id {_} {_} {_} {A} (FObj T a) ]
56 83ff8d48fdca add unitility Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	97
688 a5f2ca67e7c5 fix monad/adjunction definition Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 681 diff changeset	98 record Monad {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ)
87 4690953794c4 MEsolution Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 86 diff changeset	99 : Set (suc (c₁ ⊔ c₂ ⊔ ℓ )) where
4690953794c4 MEsolution Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 86 diff changeset	100 field
688 a5f2ca67e7c5 fix monad/adjunction definition Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 681 diff changeset	101 T : Functor A A
a5f2ca67e7c5 fix monad/adjunction definition Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 681 diff changeset	102 η : NTrans A A identityFunctor T
a5f2ca67e7c5 fix monad/adjunction definition Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 681 diff changeset	103 μ : NTrans A A (T ○ T) T
87 4690953794c4 MEsolution Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 86 diff changeset	104 isMonad : IsMonad A T η μ
130 5f331dfc000b remove Kleisli record Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 101 diff changeset	105 -- g ○ f = μ(c) T(g) f
5f331dfc000b remove Kleisli record Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 101 diff changeset	106 join : { a b : Obj A } → { c : Obj A } →
5f331dfc000b remove Kleisli record Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 101 diff changeset	107 ( Hom A b ( FObj T c )) → ( Hom A a ( FObj T b)) → Hom A a ( FObj T c )
5f331dfc000b remove Kleisli record Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 101 diff changeset	108 join {_} {_} {c} g f = A [ TMap μ c o A [ FMap T g o f ] ]
5f331dfc000b remove Kleisli record Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 101 diff changeset	109
56 83ff8d48fdca add unitility Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	110
87 4690953794c4 MEsolution Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 86 diff changeset	111 Functor*Nat : {c₁ c₂ ℓ c₁' c₂' ℓ' c₁'' c₂'' ℓ'' : Level} (A : Category c₁ c₂ ℓ) {B : Category c₁' c₂' ℓ'} (C : Category c₁'' c₂'' ℓ'')
300 d6a6dd305da2 arrow and lambda fix Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 268 diff changeset	112 (F : Functor B C) → { G H : Functor A B } → ( n : NTrans A B G H ) → NTrans A C (F ○ G) (F ○ H)
87 4690953794c4 MEsolution Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 86 diff changeset	113 Functor*Nat A {B} C F {G} {H} n = record {
300 d6a6dd305da2 arrow and lambda fix Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 268 diff changeset	114 TMap = λ a → FMap F (TMap n a)
87 4690953794c4 MEsolution Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 86 diff changeset	115 ; isNTrans = record {
130 5f331dfc000b remove Kleisli record Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 101 diff changeset	116 commute = commute
87 4690953794c4 MEsolution Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 86 diff changeset	117 }
4690953794c4 MEsolution Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 86 diff changeset	118 } where
468 c375d8f93a2c discrete category and product from a limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 460 diff changeset	119 commute : {a b : Obj A} {f : Hom A a b}
87 4690953794c4 MEsolution Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 86 diff changeset	120 → C [ C [ (FMap F ( FMap H f )) o ( FMap F (TMap n a)) ] ≈ C [ (FMap F (TMap n b )) o (FMap F (FMap G f)) ] ]
130 5f331dfc000b remove Kleisli record Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 101 diff changeset	121 commute {a} {b} {f} = let open ≈-Reasoning (C) in
468 c375d8f93a2c discrete category and product from a limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 460 diff changeset	122 begin
87 4690953794c4 MEsolution Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 86 diff changeset	123 (FMap F ( FMap H f )) o ( FMap F (TMap n a))
4690953794c4 MEsolution Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 86 diff changeset	124 ≈⟨ sym (distr F) ⟩
4690953794c4 MEsolution Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 86 diff changeset	125 FMap F ( B [ (FMap H f) o TMap n a ])
4690953794c4 MEsolution Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 86 diff changeset	126 ≈⟨ IsFunctor.≈-cong (isFunctor F) ( nat n ) ⟩
4690953794c4 MEsolution Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 86 diff changeset	127 FMap F ( B [ (TMap n b ) o FMap G f ] )
4690953794c4 MEsolution Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 86 diff changeset	128 ≈⟨ distr F ⟩
4690953794c4 MEsolution Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 86 diff changeset	129 (FMap F (TMap n b )) o (FMap F (FMap G f))
4690953794c4 MEsolution Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 86 diff changeset	130 ∎
56 83ff8d48fdca add unitility Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	131
87 4690953794c4 MEsolution Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 86 diff changeset	132 Nat*Functor : {c₁ c₂ ℓ c₁' c₂' ℓ' c₁'' c₂'' ℓ'' : Level} (A : Category c₁ c₂ ℓ) {B : Category c₁' c₂' ℓ'} (C : Category c₁'' c₂'' ℓ'')
300 d6a6dd305da2 arrow and lambda fix Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 268 diff changeset	133 { G H : Functor B C } → ( n : NTrans B C G H ) → (F : Functor A B) → NTrans A C (G ○ F) (H ○ F)
87 4690953794c4 MEsolution Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 86 diff changeset	134 Nat*Functor A {B} C {G} {H} n F = record {
300 d6a6dd305da2 arrow and lambda fix Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 268 diff changeset	135 TMap = λ a → TMap n (FObj F a)
87 4690953794c4 MEsolution Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 86 diff changeset	136 ; isNTrans = record {
130 5f331dfc000b remove Kleisli record Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 101 diff changeset	137 commute = commute
87 4690953794c4 MEsolution Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 86 diff changeset	138 }
4690953794c4 MEsolution Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 86 diff changeset	139 } where
468 c375d8f93a2c discrete category and product from a limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 460 diff changeset	140 commute : {a b : Obj A} {f : Hom A a b}
87 4690953794c4 MEsolution Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 86 diff changeset	141 → C [ C [ ( FMap H (FMap F f )) o ( TMap n (FObj F a)) ] ≈ C [ (TMap n (FObj F b )) o (FMap G (FMap F f)) ] ]
468 c375d8f93a2c discrete category and product from a limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 460 diff changeset	142 commute {a} {b} {f} = IsNTrans.commute ( isNTrans n)
56 83ff8d48fdca add unitility Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	143
87 4690953794c4 MEsolution Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 86 diff changeset	144 -- T ≃ (U_R ○ F_R)
4690953794c4 MEsolution Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 86 diff changeset	145 -- μ = U_R ε F_R
4690953794c4 MEsolution Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 86 diff changeset	146 -- nat-ε
4690953794c4 MEsolution Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 86 diff changeset	147 -- nat-η -- same as η but has different types
84 ee25f96ee8cc record Resolution Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 80 diff changeset	148
688 a5f2ca67e7c5 fix monad/adjunction definition Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 681 diff changeset	149 record MResolution {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) ( B : Category c₁' c₂' ℓ' ) ( M : Monad A )
a5f2ca67e7c5 fix monad/adjunction definition Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 681 diff changeset	150 : Set (suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁' ⊔ c₂' ⊔ ℓ' )) where
a5f2ca67e7c5 fix monad/adjunction definition Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 681 diff changeset	151 field
a5f2ca67e7c5 fix monad/adjunction definition Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 681 diff changeset	152 UR : Functor B A
a5f2ca67e7c5 fix monad/adjunction definition Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 681 diff changeset	153 FR : Functor A B
a5f2ca67e7c5 fix monad/adjunction definition Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 681 diff changeset	154 ηR : NTrans A A identityFunctor ( UR ○ FR )
a5f2ca67e7c5 fix monad/adjunction definition Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 681 diff changeset	155 εR : NTrans B B ( FR ○ UR ) identityFunctor
a5f2ca67e7c5 fix monad/adjunction definition Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 681 diff changeset	156 μR : NTrans A A ( (UR ○ FR) ○ ( UR ○ FR )) ( UR ○ FR )
a5f2ca67e7c5 fix monad/adjunction definition Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 681 diff changeset	157 Adj : IsAdjunction A B UR FR ηR εR
a5f2ca67e7c5 fix monad/adjunction definition Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 681 diff changeset	158 T=UF : Monad.T M ≃ (UR ○ FR)
a5f2ca67e7c5 fix monad/adjunction definition Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 681 diff changeset	159 μ=UεF : {x : Obj A } → A [ TMap μR x ≈ FMap UR ( TMap εR ( FObj FR x ) ) ]
300 d6a6dd305da2 arrow and lambda fix Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 268 diff changeset	160 -- ηR=η : {x : Obj A } → A [ TMap ηR x ≈ TMap η x ] -- We need T → UR FR conversion
d6a6dd305da2 arrow and lambda fix Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 268 diff changeset	161 -- μR=μ : {x : Obj A } → A [ TMap μR x ≈ TMap μ x ]
86 be4e3b073e0d resosultion Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 84 diff changeset	162
88 419923b149ca on going Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 87 diff changeset	163
350 c483374f542b try equalizer from limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 312 diff changeset	164 --
c483374f542b try equalizer from limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 312 diff changeset	165 -- e f
c483374f542b try equalizer from limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 312 diff changeset	166 -- c -------→ a ---------→ b
c483374f542b try equalizer from limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 312 diff changeset	167 -- ^ . ---------→
c483374f542b try equalizer from limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 312 diff changeset	168 -- \| . g
c483374f542b try equalizer from limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 312 diff changeset	169 -- \|k .
c483374f542b try equalizer from limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 312 diff changeset	170 -- \| . h
c483374f542b try equalizer from limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 312 diff changeset	171 -- d
c483374f542b try equalizer from limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 312 diff changeset	172
443 f526f4b68565 fix IsEqualizer Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 440 diff changeset	173 record IsEqualizer { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) {c a b : Obj A} (e : Hom A c a) (f g : Hom A a b) : Set (ℓ ⊔ (c₁ ⊔ c₂)) where
260 a87d3ea9efe4 pullback Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 253 diff changeset	174 field
a87d3ea9efe4 pullback Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 253 diff changeset	175 fe=ge : A [ A [ f o e ] ≈ A [ g o e ] ]
a87d3ea9efe4 pullback Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 253 diff changeset	176 k : {d : Obj A} (h : Hom A d a) → A [ A [ f o h ] ≈ A [ g o h ] ] → Hom A d c
a87d3ea9efe4 pullback Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 253 diff changeset	177 ek=h : {d : Obj A} → ∀ {h : Hom A d a} → {eq : A [ A [ f o h ] ≈ A [ g o h ] ] } → A [ A [ e o k {d} h eq ] ≈ h ]
a87d3ea9efe4 pullback Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 253 diff changeset	178 uniqueness : {d : Obj A} → ∀ {h : Hom A d a} → {eq : A [ A [ f o h ] ≈ A [ g o h ] ] } → {k' : Hom A d c } →
a87d3ea9efe4 pullback Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 253 diff changeset	179 A [ A [ e o k' ] ≈ h ] → A [ k {d} h eq ≈ k' ]
443 f526f4b68565 fix IsEqualizer Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 440 diff changeset	180 equalizer1 : Hom A c a
f526f4b68565 fix IsEqualizer Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 440 diff changeset	181 equalizer1 = e
260 a87d3ea9efe4 pullback Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 253 diff changeset	182
443 f526f4b68565 fix IsEqualizer Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 440 diff changeset	183 record Equalizer { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) {a b : Obj A} (f g : Hom A a b) : Set (ℓ ⊔ (c₁ ⊔ c₂)) where
440 ff36c500962e fix limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 350 diff changeset	184 field
443 f526f4b68565 fix IsEqualizer Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 440 diff changeset	185 equalizer-c : Obj A
f526f4b68565 fix IsEqualizer Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 440 diff changeset	186 equalizer : Hom A equalizer-c a
468 c375d8f93a2c discrete category and product from a limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 460 diff changeset	187 isEqualizer : IsEqualizer A equalizer f g
440 ff36c500962e fix limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 350 diff changeset	188
468 c375d8f93a2c discrete category and product from a limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 460 diff changeset	189 --
260 a87d3ea9efe4 pullback Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 253 diff changeset	190 -- Product
a87d3ea9efe4 pullback Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 253 diff changeset	191 --
264 78ce12f8e6b6 pullback done Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 260 diff changeset	192 -- c
78ce12f8e6b6 pullback done Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 260 diff changeset	193 -- f \| g
78ce12f8e6b6 pullback done Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 260 diff changeset	194 -- \|f×g
78ce12f8e6b6 pullback done Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 260 diff changeset	195 -- v
300 d6a6dd305da2 arrow and lambda fix Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 268 diff changeset	196 -- a <-------- ab ---------→ b
264 78ce12f8e6b6 pullback done Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 260 diff changeset	197 -- π1 π2
260 a87d3ea9efe4 pullback Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 253 diff changeset	198
a87d3ea9efe4 pullback Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 253 diff changeset	199
672 749df4959d19 fix completeness Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 669 diff changeset	200 record IsProduct { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) (a b ab : Obj A)
260 a87d3ea9efe4 pullback Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 253 diff changeset	201 ( π1 : Hom A ab a )
a87d3ea9efe4 pullback Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 253 diff changeset	202 ( π2 : Hom A ab b )
a87d3ea9efe4 pullback Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 253 diff changeset	203 : Set (ℓ ⊔ (c₁ ⊔ c₂)) where
a87d3ea9efe4 pullback Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 253 diff changeset	204 field
a87d3ea9efe4 pullback Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 253 diff changeset	205 _×_ : {c : Obj A} ( f : Hom A c a ) → ( g : Hom A c b ) → Hom A c ab
a87d3ea9efe4 pullback Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 253 diff changeset	206 π1fxg=f : {c : Obj A} { f : Hom A c a } → { g : Hom A c b } → A [ A [ π1 o ( f × g ) ] ≈ f ]
a87d3ea9efe4 pullback Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 253 diff changeset	207 π2fxg=g : {c : Obj A} { f : Hom A c a } → { g : Hom A c b } → A [ A [ π2 o ( f × g ) ] ≈ g ]
a87d3ea9efe4 pullback Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 253 diff changeset	208 uniqueness : {c : Obj A} { h : Hom A c ab } → A [ ( A [ π1 o h ] ) × ( A [ π2 o h ] ) ≈ h ]
468 c375d8f93a2c discrete category and product from a limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 460 diff changeset	209 ×-cong : {c : Obj A} { f f' : Hom A c a } → { g g' : Hom A c b } → A [ f ≈ f' ] → A [ g ≈ g' ] → A [ f × g ≈ f' × g' ]
440 ff36c500962e fix limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 350 diff changeset	210
681 bd8f7346f252 fix Product and pullback Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 676 diff changeset	211 record Product { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) ( a b : Obj A )
440 ff36c500962e fix limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 350 diff changeset	212 : Set (ℓ ⊔ (c₁ ⊔ c₂)) where
ff36c500962e fix limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 350 diff changeset	213 field
681 bd8f7346f252 fix Product and pullback Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 676 diff changeset	214 product : Obj A
bd8f7346f252 fix Product and pullback Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 676 diff changeset	215 π1 : Hom A product a
bd8f7346f252 fix Product and pullback Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 676 diff changeset	216 π2 : Hom A product b
bd8f7346f252 fix Product and pullback Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 676 diff changeset	217 isProduct : IsProduct A a b product π1 π2
260 a87d3ea9efe4 pullback Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 253 diff changeset	218
468 c375d8f93a2c discrete category and product from a limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 460 diff changeset	219 -----
c375d8f93a2c discrete category and product from a limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 460 diff changeset	220 --
c375d8f93a2c discrete category and product from a limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 460 diff changeset	221 -- product on arbitrary index
c375d8f93a2c discrete category and product from a limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 460 diff changeset	222 --
c375d8f93a2c discrete category and product from a limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 460 diff changeset	223
691 917e51be9bbf change argument of Limit and K Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 690 diff changeset	224 record IsIProduct { c c₁ c₂ ℓ : Level} ( I : Set c) ( A : Category c₁ c₂ ℓ )
468 c375d8f93a2c discrete category and product from a limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 460 diff changeset	225 ( p : Obj A ) -- product
c375d8f93a2c discrete category and product from a limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 460 diff changeset	226 ( ai : I → Obj A ) -- families
508 3ce21b2a671a IProduct is written in Sets Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 495 diff changeset	227 ( pi : (i : I ) → Hom A p ( ai i ) ) -- projections
468 c375d8f93a2c discrete category and product from a limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 460 diff changeset	228 : Set (c ⊔ ℓ ⊔ (c₁ ⊔ c₂)) where
c375d8f93a2c discrete category and product from a limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 460 diff changeset	229 field
c375d8f93a2c discrete category and product from a limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 460 diff changeset	230 iproduct : {q : Obj A} → ( qi : (i : I) → Hom A q (ai i) ) → Hom A q p
676 faf48511f69d two product as in CWM Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 673 diff changeset	231 pif=q : {q : Obj A} → { qi : (i : I) → Hom A q (ai i) }
faf48511f69d two product as in CWM Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 673 diff changeset	232 → ∀ { i : I } → A [ A [ ( pi i ) o ( iproduct qi ) ] ≈ (qi i) ]
468 c375d8f93a2c discrete category and product from a limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 460 diff changeset	233 ip-uniqueness : {q : Obj A} { h : Hom A q p } → A [ iproduct ( λ (i : I) → A [ (pi i) o h ] ) ≈ h ]
c375d8f93a2c discrete category and product from a limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 460 diff changeset	234 ip-cong : {q : Obj A} → { qi : (i : I) → Hom A q (ai i) } → { qi' : (i : I) → Hom A q (ai i) }
c375d8f93a2c discrete category and product from a limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 460 diff changeset	235 → ( ∀ (i : I ) → A [ qi i ≈ qi' i ] ) → A [ iproduct qi ≈ iproduct qi' ]
c375d8f93a2c discrete category and product from a limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 460 diff changeset	236 -- another form of uniquness
c375d8f93a2c discrete category and product from a limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 460 diff changeset	237 ip-uniqueness1 : {q : Obj A} → ( qi : (i : I) → Hom A q (ai i) ) → ( product' : Hom A q p )
c375d8f93a2c discrete category and product from a limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 460 diff changeset	238 → ( ∀ { i : I } → A [ A [ ( pi i ) o product' ] ≈ (qi i) ] )
c375d8f93a2c discrete category and product from a limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 460 diff changeset	239 → A [ product' ≈ iproduct qi ]
c375d8f93a2c discrete category and product from a limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 460 diff changeset	240 ip-uniqueness1 {a} qi product' eq = let open ≈-Reasoning (A) in begin
c375d8f93a2c discrete category and product from a limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 460 diff changeset	241 product'
c375d8f93a2c discrete category and product from a limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 460 diff changeset	242 ≈↑⟨ ip-uniqueness ⟩
c375d8f93a2c discrete category and product from a limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 460 diff changeset	243 iproduct (λ i₁ → A [ pi i₁ o product' ])
c375d8f93a2c discrete category and product from a limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 460 diff changeset	244 ≈⟨ ip-cong ( λ i → begin
c375d8f93a2c discrete category and product from a limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 460 diff changeset	245 pi i o product'
c375d8f93a2c discrete category and product from a limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 460 diff changeset	246 ≈⟨ eq {i} ⟩
c375d8f93a2c discrete category and product from a limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 460 diff changeset	247 qi i
c375d8f93a2c discrete category and product from a limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 460 diff changeset	248 ∎ ) ⟩
c375d8f93a2c discrete category and product from a limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 460 diff changeset	249 iproduct qi
c375d8f93a2c discrete category and product from a limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 460 diff changeset	250 ∎
c375d8f93a2c discrete category and product from a limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 460 diff changeset	251
691 917e51be9bbf change argument of Limit and K Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 690 diff changeset	252 record IProduct { c c₁ c₂ ℓ : Level} ( I : Set c) ( A : Category c₁ c₂ ℓ ) (ai : I → Obj A) : Set (c ⊔ ℓ ⊔ (c₁ ⊔ c₂)) where
508 3ce21b2a671a IProduct is written in Sets Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 495 diff changeset	253 field
3ce21b2a671a IProduct is written in Sets Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 495 diff changeset	254 iprod : Obj A
3ce21b2a671a IProduct is written in Sets Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 495 diff changeset	255 pi : (i : I ) → Hom A iprod ( ai i )
691 917e51be9bbf change argument of Limit and K Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 690 diff changeset	256 isIProduct : IsIProduct I A iprod ai pi
508 3ce21b2a671a IProduct is written in Sets Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 495 diff changeset	257
468 c375d8f93a2c discrete category and product from a limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 460 diff changeset	258
260 a87d3ea9efe4 pullback Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 253 diff changeset	259 -- Pullback
a87d3ea9efe4 pullback Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 253 diff changeset	260 -- f
300 d6a6dd305da2 arrow and lambda fix Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 268 diff changeset	261 -- a ------→ c
468 c375d8f93a2c discrete category and product from a limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 460 diff changeset	262 -- ^ ^
260 a87d3ea9efe4 pullback Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 253 diff changeset	263 -- π1 \| \|g
a87d3ea9efe4 pullback Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 253 diff changeset	264 -- \| \|
300 d6a6dd305da2 arrow and lambda fix Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 268 diff changeset	265 -- ab ------→ b
260 a87d3ea9efe4 pullback Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 253 diff changeset	266 -- ^ π2
a87d3ea9efe4 pullback Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 253 diff changeset	267 -- \|
468 c375d8f93a2c discrete category and product from a limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 460 diff changeset	268 -- d
260 a87d3ea9efe4 pullback Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 253 diff changeset	269 --
681 bd8f7346f252 fix Product and pullback Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 676 diff changeset	270 record IsPullback { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) {a b c ab : Obj A}
260 a87d3ea9efe4 pullback Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 253 diff changeset	271 ( f : Hom A a c ) ( g : Hom A b c )
a87d3ea9efe4 pullback Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 253 diff changeset	272 ( π1 : Hom A ab a ) ( π2 : Hom A ab b )
a87d3ea9efe4 pullback Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 253 diff changeset	273 : Set (ℓ ⊔ (c₁ ⊔ c₂)) where
a87d3ea9efe4 pullback Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 253 diff changeset	274 field
a87d3ea9efe4 pullback Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 253 diff changeset	275 commute : A [ A [ f o π1 ] ≈ A [ g o π2 ] ]
681 bd8f7346f252 fix Product and pullback Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 676 diff changeset	276 pullback : { d : Obj A } → { π1' : Hom A d a } { π2' : Hom A d b } → A [ A [ f o π1' ] ≈ A [ g o π2' ] ] → Hom A d ab
468 c375d8f93a2c discrete category and product from a limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 460 diff changeset	277 π1p=π1 : { d : Obj A } → { π1' : Hom A d a } { π2' : Hom A d b } → { eq : A [ A [ f o π1' ] ≈ A [ g o π2' ] ] }
681 bd8f7346f252 fix Product and pullback Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 676 diff changeset	278 → A [ A [ π1 o pullback eq ] ≈ π1' ]
468 c375d8f93a2c discrete category and product from a limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 460 diff changeset	279 π2p=π2 : { d : Obj A } → { π1' : Hom A d a } { π2' : Hom A d b } → { eq : A [ A [ f o π1' ] ≈ A [ g o π2' ] ] }
681 bd8f7346f252 fix Product and pullback Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 676 diff changeset	280 → A [ A [ π2 o pullback eq ] ≈ π2' ]
468 c375d8f93a2c discrete category and product from a limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 460 diff changeset	281 uniqueness : { d : Obj A } → ( p' : Hom A d ab ) → { π1' : Hom A d a } { π2' : Hom A d b } → { eq : A [ A [ f o π1' ] ≈ A [ g o π2' ] ] }
260 a87d3ea9efe4 pullback Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 253 diff changeset	282 → { π1p=π1' : A [ A [ π1 o p' ] ≈ π1' ] }
a87d3ea9efe4 pullback Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 253 diff changeset	283 → { π2p=π2' : A [ A [ π2 o p' ] ≈ π2' ] }
681 bd8f7346f252 fix Product and pullback Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 676 diff changeset	284 → A [ pullback eq ≈ p' ]
bd8f7346f252 fix Product and pullback Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 676 diff changeset	285
bd8f7346f252 fix Product and pullback Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 676 diff changeset	286 record Pullback { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) {a b c : Obj A}
bd8f7346f252 fix Product and pullback Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 676 diff changeset	287 ( f : Hom A a c ) ( g : Hom A b c )
bd8f7346f252 fix Product and pullback Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 676 diff changeset	288 : Set (ℓ ⊔ (c₁ ⊔ c₂)) where
bd8f7346f252 fix Product and pullback Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 676 diff changeset	289 field
bd8f7346f252 fix Product and pullback Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 676 diff changeset	290 ab : Obj A
bd8f7346f252 fix Product and pullback Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 676 diff changeset	291 π1 : Hom A ab a
bd8f7346f252 fix Product and pullback Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 676 diff changeset	292 π2 : Hom A ab b
bd8f7346f252 fix Product and pullback Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 676 diff changeset	293 isPullback : IsPullback A f g π1 π2
312 702adc45704f is this right direction? Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 300 diff changeset	294
702adc45704f is this right direction? Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 300 diff changeset	295 --
702adc45704f is this right direction? Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 300 diff changeset	296 -- Limit
702adc45704f is this right direction? Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 300 diff changeset	297 --
702adc45704f is this right direction? Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 300 diff changeset	298 -----
702adc45704f is this right direction? Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 300 diff changeset	299
702adc45704f is this right direction? Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 300 diff changeset	300 -- Constancy Functor
702adc45704f is this right direction? Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 300 diff changeset	301
691 917e51be9bbf change argument of Limit and K Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 690 diff changeset	302 K : { c₁' c₂' ℓ' : Level} (I : Category c₁' c₂' ℓ') { c₁'' c₂'' ℓ'' : Level} ( A : Category c₁'' c₂'' ℓ'' )
312 702adc45704f is this right direction? Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 300 diff changeset	303 → ( a : Obj A ) → Functor I A
691 917e51be9bbf change argument of Limit and K Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 690 diff changeset	304 K I A a = record {
312 702adc45704f is this right direction? Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 300 diff changeset	305 FObj = λ i → a ;
702adc45704f is this right direction? Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 300 diff changeset	306 FMap = λ f → id1 A a ;
702adc45704f is this right direction? Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 300 diff changeset	307 isFunctor = let open ≈-Reasoning (A) in record {
702adc45704f is this right direction? Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 300 diff changeset	308 ≈-cong = λ f=g → refl-hom
702adc45704f is this right direction? Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 300 diff changeset	309 ; identity = refl-hom
702adc45704f is this right direction? Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 300 diff changeset	310 ; distr = sym idL
702adc45704f is this right direction? Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 300 diff changeset	311 }
702adc45704f is this right direction? Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 300 diff changeset	312 }
702adc45704f is this right direction? Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 300 diff changeset	313
702adc45704f is this right direction? Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 300 diff changeset	314
691 917e51be9bbf change argument of Limit and K Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 690 diff changeset	315 record IsLimit { c₁ c₂ ℓ : Level} { c₁' c₂' ℓ' : Level} ( I : Category c₁ c₂ ℓ ) ( A : Category c₁' c₂' ℓ' ) ( Γ : Functor I A )
917e51be9bbf change argument of Limit and K Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 690 diff changeset	316 (a0 : Obj A ) (t0 : NTrans I A ( K I A a0 ) Γ ) : Set (suc (c₁' ⊔ c₂' ⊔ ℓ' ⊔ c₁ ⊔ c₂ ⊔ ℓ )) where
312 702adc45704f is this right direction? Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 300 diff changeset	317 field
691 917e51be9bbf change argument of Limit and K Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 690 diff changeset	318 limit : ( a : Obj A ) → ( t : NTrans I A ( K I A a ) Γ ) → Hom A a a0
917e51be9bbf change argument of Limit and K Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 690 diff changeset	319 t0f=t : { a : Obj A } → { t : NTrans I A ( K I A a ) Γ } → ∀ { i : Obj I } →
312 702adc45704f is this right direction? Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 300 diff changeset	320 A [ A [ TMap t0 i o limit a t ] ≈ TMap t i ]
691 917e51be9bbf change argument of Limit and K Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 690 diff changeset	321 limit-uniqueness : { a : Obj A } → { t : NTrans I A ( K I A a ) Γ } → { f : Hom A a a0 } → ( ∀ { i : Obj I } →
312 702adc45704f is this right direction? Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 300 diff changeset	322 A [ A [ TMap t0 i o f ] ≈ TMap t i ] ) → A [ limit a t ≈ f ]
702adc45704f is this right direction? Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 300 diff changeset	323
691 917e51be9bbf change argument of Limit and K Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 690 diff changeset	324 record Limit { c₁ c₂ ℓ : Level} { c₁' c₂' ℓ' : Level} ( I : Category c₁ c₂ ℓ ) ( A : Category c₁' c₂' ℓ' ) ( Γ : Functor I A )
487 c257347a27f3 found limit in freyd Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 484 diff changeset	325 : Set (suc (c₁' ⊔ c₂' ⊔ ℓ' ⊔ c₁ ⊔ c₂ ⊔ ℓ )) where
c257347a27f3 found limit in freyd Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 484 diff changeset	326 field
c257347a27f3 found limit in freyd Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 484 diff changeset	327 a0 : Obj A
691 917e51be9bbf change argument of Limit and K Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 690 diff changeset	328 t0 : NTrans I A ( K I A a0 ) Γ
917e51be9bbf change argument of Limit and K Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 690 diff changeset	329 isLimit : IsLimit I A Γ a0 t0
487 c257347a27f3 found limit in freyd Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 484 diff changeset	330
691 917e51be9bbf change argument of Limit and K Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 690 diff changeset	331 LimitNat : { c₁' c₂' ℓ' : Level} (I : Category c₁' c₂' ℓ') { c₁ c₂ ℓ : Level} ( B : Category c₁ c₂ ℓ ) { c₁'' c₂'' ℓ'' : Level}
487 c257347a27f3 found limit in freyd Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 484 diff changeset	332 ( C : Category c₁'' c₂'' ℓ'' )
c257347a27f3 found limit in freyd Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 484 diff changeset	333 ( Γ : Functor I B )
691 917e51be9bbf change argument of Limit and K Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 690 diff changeset	334 ( lim : Obj B ) ( tb : NTrans I B ( K I B lim ) Γ ) →
917e51be9bbf change argument of Limit and K Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 690 diff changeset	335 ( U : Functor B C) → NTrans I C ( K I C (FObj U lim) ) (U ○ Γ)
917e51be9bbf change argument of Limit and K Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 690 diff changeset	336 LimitNat I B C Γ lim tb U = record {
487 c257347a27f3 found limit in freyd Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 484 diff changeset	337 TMap = TMap (Functor*Nat I C U tb) ;
c257347a27f3 found limit in freyd Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 484 diff changeset	338 isNTrans = record { commute = λ {a} {b} {f} → let open ≈-Reasoning (C) in begin
c257347a27f3 found limit in freyd Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 484 diff changeset	339 FMap (U ○ Γ) f o TMap (Functor*Nat I C U tb) a
c257347a27f3 found limit in freyd Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 484 diff changeset	340 ≈⟨ nat ( Functor*Nat I C U tb ) ⟩
691 917e51be9bbf change argument of Limit and K Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 690 diff changeset	341 TMap (Functor*Nat I C U tb) b o FMap (U ○ K I B lim) f
487 c257347a27f3 found limit in freyd Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 484 diff changeset	342 ≈⟨ cdr (IsFunctor.identity (isFunctor U) ) ⟩
691 917e51be9bbf change argument of Limit and K Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 690 diff changeset	343 TMap (Functor*Nat I C U tb) b o FMap (K I C (FObj U lim)) f
487 c257347a27f3 found limit in freyd Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 484 diff changeset	344 ∎
c257347a27f3 found limit in freyd Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 484 diff changeset	345 } }
c257347a27f3 found limit in freyd Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 484 diff changeset	346
c257347a27f3 found limit in freyd Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 484 diff changeset	347 open Limit
691 917e51be9bbf change argument of Limit and K Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 690 diff changeset	348 record LimitPreserve { c₁ c₂ ℓ : Level} { c₁' c₂' ℓ' : Level} ( I : Category c₁ c₂ ℓ ) ( A : Category c₁' c₂' ℓ' )
487 c257347a27f3 found limit in freyd Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 484 diff changeset	349 { c₁'' c₂'' ℓ'' : Level} ( C : Category c₁'' c₂'' ℓ'' )
c257347a27f3 found limit in freyd Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 484 diff changeset	350 (G : Functor A C) : Set (suc (c₁' ⊔ c₂' ⊔ ℓ' ⊔ c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁'' ⊔ c₂'' ⊔ ℓ'' )) where
c257347a27f3 found limit in freyd Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 484 diff changeset	351 field
691 917e51be9bbf change argument of Limit and K Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 690 diff changeset	352 preserve : ( Γ : Functor I A ) → ( limita : Limit I A Γ ) →
917e51be9bbf change argument of Limit and K Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 690 diff changeset	353 IsLimit I C (G ○ Γ) (FObj G (a0 limita ) ) (LimitNat I A C Γ (a0 limita ) (t0 limita) G )
917e51be9bbf change argument of Limit and K Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 690 diff changeset	354 plimit : { Γ : Functor I A } → ( limita : Limit I A Γ ) → Limit I C (G ○ Γ )
492 c7b8017bcd4d on going.. Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 487 diff changeset	355 plimit {Γ} limita = record { a0 = (FObj G (a0 limita ))
691 917e51be9bbf change argument of Limit and K Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 690 diff changeset	356 ; t0 = LimitNat I A C Γ (a0 limita ) (t0 limita) G
487 c257347a27f3 found limit in freyd Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 484 diff changeset	357 ; isLimit = preserve Γ limita }
c257347a27f3 found limit in freyd Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 484 diff changeset	358
691 917e51be9bbf change argument of Limit and K Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 690 diff changeset	359 record CreateLimit { c₁' c₂' ℓ' : Level} { c₁ c₂ ℓ : Level} ( I : Category c₁ c₂ ℓ ) ( A : Category c₁' c₂' ℓ' )
440 ff36c500962e fix limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 350 diff changeset	360 : Set (suc (c₁' ⊔ c₂' ⊔ ℓ' ⊔ c₁ ⊔ c₂ ⊔ ℓ )) where
ff36c500962e fix limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 350 diff changeset	361 field
691 917e51be9bbf change argument of Limit and K Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 690 diff changeset	362 climit : ( Γ : Functor I A ) → Limit I A Γ
440 ff36c500962e fix limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 350 diff changeset	363
468 c375d8f93a2c discrete category and product from a limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 460 diff changeset	364 record Complete { c₁' c₂' ℓ' : Level} { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) ( I : Category c₁' c₂' ℓ' )
440 ff36c500962e fix limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 350 diff changeset	365 : Set (suc (c₁' ⊔ c₂' ⊔ ℓ' ⊔ c₁ ⊔ c₂ ⊔ ℓ )) where
ff36c500962e fix limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 350 diff changeset	366 field
691 917e51be9bbf change argument of Limit and K Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 690 diff changeset	367 climit : ( Γ : Functor I A ) → Limit I A Γ
917e51be9bbf change argument of Limit and K Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 690 diff changeset	368 cproduct : ( I : Set c₁' ) (fi : I → Obj A ) → IProduct I A fi -- c₁ should be a free level
672 749df4959d19 fix completeness Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 669 diff changeset	369 cequalizer : {a b : Obj A} (f g : Hom A a b) → Equalizer A f g
484 fcae3025d900 fix Limit pu a0 and t0 in record definition Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 468 diff changeset	370 open Limit
672 749df4959d19 fix completeness Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 669 diff changeset	371 limit-c : ( Γ : Functor I A ) → Obj A
487 c257347a27f3 found limit in freyd Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 484 diff changeset	372 limit-c Γ = a0 ( climit Γ)
691 917e51be9bbf change argument of Limit and K Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 690 diff changeset	373 limit-u : ( Γ : Functor I A ) → NTrans I A ( K I A (limit-c Γ )) Γ
487 c257347a27f3 found limit in freyd Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 484 diff changeset	374 limit-u Γ = t0 ( climit Γ)
672 749df4959d19 fix completeness Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 669 diff changeset	375 open Equalizer
749df4959d19 fix completeness Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 669 diff changeset	376 equalizer-p : {a b : Obj A} (f g : Hom A a b) → Obj A
749df4959d19 fix completeness Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 669 diff changeset	377 equalizer-p f g = equalizer-c (cequalizer f g )
749df4959d19 fix completeness Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 669 diff changeset	378 equalizer-e : {a b : Obj A} (f g : Hom A a b) → Hom A (equalizer-p f g) a
749df4959d19 fix completeness Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 669 diff changeset	379 equalizer-e f g = equalizer (cequalizer f g )
526 b035cd3be525 Small Category for Sets Limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 508 diff changeset	380
662 e1d54c0f73a7 move InitialObject to cat-utility Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 526 diff changeset	381
e1d54c0f73a7 move InitialObject to cat-utility Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 526 diff changeset	382 -- initial object
e1d54c0f73a7 move InitialObject to cat-utility Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 526 diff changeset	383
688 a5f2ca67e7c5 fix monad/adjunction definition Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 681 diff changeset	384 record IsInitialObject {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (i : Obj A) : Set (suc ℓ ⊔ (suc c₁ ⊔ suc c₂)) where
662 e1d54c0f73a7 move InitialObject to cat-utility Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 526 diff changeset	385 field
e1d54c0f73a7 move InitialObject to cat-utility Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 526 diff changeset	386 initial : ∀( a : Obj A ) → Hom A i a
e1d54c0f73a7 move InitialObject to cat-utility Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 526 diff changeset	387 uniqueness : { a : Obj A } → ( f : Hom A i a ) → A [ f ≈ initial a ]
e1d54c0f73a7 move InitialObject to cat-utility Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 526 diff changeset	388
688 a5f2ca67e7c5 fix monad/adjunction definition Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 681 diff changeset	389 record InitialObject {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) : Set (suc ℓ ⊔ (suc c₁ ⊔ suc c₂)) where
a5f2ca67e7c5 fix monad/adjunction definition Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 681 diff changeset	390 field
a5f2ca67e7c5 fix monad/adjunction definition Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 681 diff changeset	391 initialObject : Obj A
a5f2ca67e7c5 fix monad/adjunction definition Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 681 diff changeset	392 isInitialObject : IsInitialObject A initialObject
a5f2ca67e7c5 fix monad/adjunction definition Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 681 diff changeset	393

Mercurial > hg > Members > kono > Proof > category

annotate cat-utility.agda @ 694:2043f7fd4273