Mercurial > hg > Members > kono > Proof > category

annotate src/cat-utility.agda @ 970:72b6b4577911

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Fri, 26 Feb 2021 12:19:58 +0900
parents 3a096cb82dc4
children 9746e93a8c31
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
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
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
731
117e5b392673 Generalize Free Theorem
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 695
diff changeset
16 record Iso {c₁ c₂ ℓ : Level} (C : Category c₁ c₂ ℓ)
117e5b392673 Generalize Free Theorem
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 695
diff changeset
17 (x y : Obj C )
117e5b392673 Generalize Free Theorem
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 695
diff changeset
18 : Set ( suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁)) where
117e5b392673 Generalize Free Theorem
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 695
diff changeset
19 field
117e5b392673 Generalize Free Theorem
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 695
diff changeset
20 ≅→ : Hom C x y
117e5b392673 Generalize Free Theorem
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 695
diff changeset
21 ≅← : Hom C y x
117e5b392673 Generalize Free Theorem
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 695
diff changeset
22 iso→ : C [ C [ ≅← o ≅→ ] ≈ id1 C x ]
117e5b392673 Generalize Free Theorem
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 695
diff changeset
23 iso← : C [ C [ ≅→ o ≅← ] ≈ id1 C y ]
117e5b392673 Generalize Free Theorem
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 695
diff changeset
24
117e5b392673 Generalize Free Theorem
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 695
diff changeset
25
468
c375d8f93a2c discrete category and product from a limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 460
diff changeset
26 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
27 ( U : Functor B A )
4690953794c4 MEsolution
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 86
diff changeset
28 ( F : Obj A → Obj B )
4690953794c4 MEsolution
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 86
diff changeset
29 ( η : (a : Obj A) → Hom A a ( FObj U (F a) ) )
4690953794c4 MEsolution
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 86
diff changeset
30 ( _* : { 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
31 : Set (suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁' ⊔ c₂' ⊔ ℓ' )) where
4690953794c4 MEsolution
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 86
diff changeset
32 field
468
c375d8f93a2c discrete category and product from a limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 460
diff changeset
33 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
34 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
35 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
36 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
37
468
c375d8f93a2c discrete category and product from a limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 460
diff changeset
38 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
39 ( U : Functor B A )
87
4690953794c4 MEsolution
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 86
diff changeset
40 : Set (suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁' ⊔ c₂' ⊔ ℓ' )) where
4690953794c4 MEsolution
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 86
diff changeset
41 infixr 11 _*
4690953794c4 MEsolution
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 86
diff changeset
42 field
690
3d41a8edbf63 fix universal mapping done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 689
diff changeset
43 F : Obj A → Obj B
3d41a8edbf63 fix universal mapping done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 689
diff changeset
44 η : (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
45 _* : { 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
46 isUniversalMapping : IsUniversalMapping A B U F η _*
56
83ff8d48fdca add unitility
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
47
468
c375d8f93a2c discrete category and product from a limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 460
diff changeset
48 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
49 ( F : Functor A B )
2ff44ee3cb32 co universal mapping
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 265
diff changeset
50 ( U : Obj B → Obj A )
2ff44ee3cb32 co universal mapping
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 265
diff changeset
51 ( ε : (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
52 ( _*' : { 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
53 : Set (suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁' ⊔ c₂' ⊔ ℓ' )) where
2ff44ee3cb32 co universal mapping
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 265
diff changeset
54 field
468
c375d8f93a2c discrete category and product from a limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 460
diff changeset
55 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
56 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
57 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
58 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
59
468
c375d8f93a2c discrete category and product from a limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 460
diff changeset
60 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
61 ( F : Functor A B )
268
2ff44ee3cb32 co universal mapping
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 265
diff changeset
62 : Set (suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁' ⊔ c₂' ⊔ ℓ' )) where
2ff44ee3cb32 co universal mapping
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 265
diff changeset
63 infixr 11 _*'
2ff44ee3cb32 co universal mapping
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 265
diff changeset
64 field
690
3d41a8edbf63 fix universal mapping done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 689
diff changeset
65 U : Obj B → Obj A
3d41a8edbf63 fix universal mapping done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 689
diff changeset
66 ε : (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
67 _*' : { 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
68 iscoUniversalMapping : coIsUniversalMapping A B F U ε _*'
2ff44ee3cb32 co universal mapping
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 265
diff changeset
69
87
4690953794c4 MEsolution
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 86
diff changeset
70 open NTrans
4690953794c4 MEsolution
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 86
diff changeset
71 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
72 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
73 ( U : Functor B A )
4690953794c4 MEsolution
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 86
diff changeset
74 ( F : Functor A B )
4690953794c4 MEsolution
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 86
diff changeset
75 ( η : NTrans A A identityFunctor ( U ○ F ) )
4690953794c4 MEsolution
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 86
diff changeset
76 ( ε : NTrans B B ( F ○ U ) identityFunctor )
4690953794c4 MEsolution
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 86
diff changeset
77 : Set (suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁' ⊔ c₂' ⊔ ℓ' )) where
4690953794c4 MEsolution
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 86
diff changeset
78 field
4690953794c4 MEsolution
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 86
diff changeset
79 adjoint1 : { b : Obj B } →
4690953794c4 MEsolution
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 86
diff changeset
80 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
81 adjoint2 : {a : Obj A} →
4690953794c4 MEsolution
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 86
diff changeset
82 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
83
468
c375d8f93a2c discrete category and product from a limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 460
diff changeset
84 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
85 : Set (suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁' ⊔ c₂' ⊔ ℓ' )) where
4690953794c4 MEsolution
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 86
diff changeset
86 field
688
a5f2ca67e7c5 fix monad/adjunction definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 681
diff changeset
87 U : Functor B A
a5f2ca67e7c5 fix monad/adjunction definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 681
diff changeset
88 F : Functor A B
a5f2ca67e7c5 fix monad/adjunction definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 681
diff changeset
89 η : NTrans A A identityFunctor ( U ○ F )
a5f2ca67e7c5 fix monad/adjunction definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 681
diff changeset
90 ε : NTrans B B ( F ○ U ) identityFunctor
87
4690953794c4 MEsolution
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 86
diff changeset
91 isAdjunction : IsAdjunction A B U F η ε
202
58ee98bbb333 remove an extensionality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 176
diff changeset
92 U-functor = U
58ee98bbb333 remove an extensionality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 176
diff changeset
93 F-functor = F
58ee98bbb333 remove an extensionality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 176
diff changeset
94 Eta = η
58ee98bbb333 remove an extensionality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 176
diff changeset
95 Epsiron = ε
56
83ff8d48fdca add unitility
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
96
83ff8d48fdca add unitility
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
97
468
c375d8f93a2c discrete category and product from a limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 460
diff changeset
98 record IsMonad {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ)
87
4690953794c4 MEsolution
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 86
diff changeset
99 ( T : Functor A A )
4690953794c4 MEsolution
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 86
diff changeset
100 ( η : NTrans A A identityFunctor T )
4690953794c4 MEsolution
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 86
diff changeset
101 ( μ : NTrans A A (T ○ T) T)
4690953794c4 MEsolution
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 86
diff changeset
102 : Set (suc (c₁ ⊔ c₂ ⊔ ℓ )) where
4690953794c4 MEsolution
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 86
diff changeset
103 field
4690953794c4 MEsolution
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 86
diff changeset
104 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
105 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
106 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
107
688
a5f2ca67e7c5 fix monad/adjunction definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 681
diff changeset
108 record Monad {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ)
87
4690953794c4 MEsolution
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 86
diff changeset
109 : Set (suc (c₁ ⊔ c₂ ⊔ ℓ )) where
4690953794c4 MEsolution
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 86
diff changeset
110 field
688
a5f2ca67e7c5 fix monad/adjunction definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 681
diff changeset
111 T : Functor A A
a5f2ca67e7c5 fix monad/adjunction definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 681
diff changeset
112 η : NTrans A A identityFunctor T
a5f2ca67e7c5 fix monad/adjunction definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 681
diff changeset
113 μ : NTrans A A (T ○ T) T
87
4690953794c4 MEsolution
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 86
diff changeset
114 isMonad : IsMonad A T η μ
130
5f331dfc000b remove Kleisli record
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 101
diff changeset
115 -- g ○ f = μ(c) T(g) f
5f331dfc000b remove Kleisli record
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 101
diff changeset
116 join : { a b : Obj A } → { c : Obj A } →
5f331dfc000b remove Kleisli record
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 101
diff changeset
117 ( 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
118 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
119
968
3a096cb82dc4 Polynominal category and functional completeness begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 949
diff changeset
120 record IsCoMonad {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ)
3a096cb82dc4 Polynominal category and functional completeness begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 949
diff changeset
121 ( S : Functor A A )
3a096cb82dc4 Polynominal category and functional completeness begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 949
diff changeset
122 ( ε : NTrans A A S identityFunctor )
3a096cb82dc4 Polynominal category and functional completeness begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 949
diff changeset
123 ( δ : NTrans A A S (S ○ S) )
3a096cb82dc4 Polynominal category and functional completeness begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 949
diff changeset
124 : Set (suc (c₁ ⊔ c₂ ⊔ ℓ )) where
3a096cb82dc4 Polynominal category and functional completeness begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 949
diff changeset
125 field
3a096cb82dc4 Polynominal category and functional completeness begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 949
diff changeset
126 assoc : {a : Obj A} → A [ A [ TMap δ (FObj S a) o TMap δ a ] ≈ A [ FMap S (TMap δ a) o TMap δ a ] ]
3a096cb82dc4 Polynominal category and functional completeness begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 949
diff changeset
127 unity1 : {a : Obj A} → A [ A [ TMap ε ( FObj S a ) o TMap δ a ] ≈ Id {_} {_} {_} {A} (FObj S a) ]
3a096cb82dc4 Polynominal category and functional completeness begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 949
diff changeset
128 unity2 : {a : Obj A} → A [ A [ (FMap S (TMap ε a )) o TMap δ a ] ≈ Id {_} {_} {_} {A} (FObj S a) ]
3a096cb82dc4 Polynominal category and functional completeness begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 949
diff changeset
129
3a096cb82dc4 Polynominal category and functional completeness begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 949
diff changeset
130 record coMonad {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (S : Functor A A)
3a096cb82dc4 Polynominal category and functional completeness begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 949
diff changeset
131 : Set (suc (c₁ ⊔ c₂ ⊔ ℓ )) where
3a096cb82dc4 Polynominal category and functional completeness begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 949
diff changeset
132 field
3a096cb82dc4 Polynominal category and functional completeness begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 949
diff changeset
133 ε : NTrans A A S identityFunctor
3a096cb82dc4 Polynominal category and functional completeness begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 949
diff changeset
134 δ : NTrans A A S (S ○ S)
3a096cb82dc4 Polynominal category and functional completeness begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 949
diff changeset
135 isCoMonad : IsCoMonad A S ε δ
3a096cb82dc4 Polynominal category and functional completeness begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 949
diff changeset
136 -- g ○ f = g S(f) δ(a)
3a096cb82dc4 Polynominal category and functional completeness begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 949
diff changeset
137 coJoin : { a b : Obj A } → { c : Obj A } →
3a096cb82dc4 Polynominal category and functional completeness begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 949
diff changeset
138 ( Hom A (FObj S b ) c ) → ( Hom A ( FObj S a) b ) → Hom A ( FObj S a ) c
3a096cb82dc4 Polynominal category and functional completeness begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 949
diff changeset
139 coJoin {a} {_} {_} g f = A [ A [ g o FMap S f ] o TMap δ a ]
3a096cb82dc4 Polynominal category and functional completeness begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 949
diff changeset
140
56
83ff8d48fdca add unitility
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
141
87
4690953794c4 MEsolution
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 86
diff changeset
142 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
143 (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
144 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
145 TMap = λ a → FMap F (TMap n a)
87
4690953794c4 MEsolution
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 86
diff changeset
146 ; isNTrans = record {
130
5f331dfc000b remove Kleisli record
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 101
diff changeset
147 commute = commute
87
4690953794c4 MEsolution
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 86
diff changeset
148 }
4690953794c4 MEsolution
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 86
diff changeset
149 } where
468
c375d8f93a2c discrete category and product from a limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 460
diff changeset
150 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
151 → 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
152 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
153 begin
87
4690953794c4 MEsolution
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 86
diff changeset
154 (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
155 ≈⟨ sym (distr F) ⟩
4690953794c4 MEsolution
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 86
diff changeset
156 FMap F ( B [ (FMap H f) o TMap n a ])
4690953794c4 MEsolution
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 86
diff changeset
157 ≈⟨ IsFunctor.≈-cong (isFunctor F) ( nat n ) ⟩
4690953794c4 MEsolution
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 86
diff changeset
158 FMap F ( B [ (TMap n b ) o FMap G f ] )
4690953794c4 MEsolution
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 86
diff changeset
159 ≈⟨ distr F ⟩
4690953794c4 MEsolution
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 86
diff changeset
160 (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
161 ∎
56
83ff8d48fdca add unitility
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
162
87
4690953794c4 MEsolution
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 86
diff changeset
163 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
164 { 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
165 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
166 TMap = λ a → TMap n (FObj F a)
87
4690953794c4 MEsolution
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 86
diff changeset
167 ; isNTrans = record {
130
5f331dfc000b remove Kleisli record
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 101
diff changeset
168 commute = commute
87
4690953794c4 MEsolution
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 86
diff changeset
169 }
4690953794c4 MEsolution
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 86
diff changeset
170 } where
468
c375d8f93a2c discrete category and product from a limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 460
diff changeset
171 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
172 → 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
173 commute {a} {b} {f} = IsNTrans.commute ( isNTrans n)
56
83ff8d48fdca add unitility
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
174
87
4690953794c4 MEsolution
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 86
diff changeset
175 -- T ≃ (U_R ○ F_R)
4690953794c4 MEsolution
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 86
diff changeset
176 -- μ = U_R ε F_R
4690953794c4 MEsolution
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 86
diff changeset
177 -- nat-ε
4690953794c4 MEsolution
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 86
diff changeset
178 -- nat-η -- same as η but has different types
84
ee25f96ee8cc record Resolution
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 80
diff changeset
179
688
a5f2ca67e7c5 fix monad/adjunction definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 681
diff changeset
180 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
181 : Set (suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁' ⊔ c₂' ⊔ ℓ' )) where
a5f2ca67e7c5 fix monad/adjunction definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 681
diff changeset
182 field
a5f2ca67e7c5 fix monad/adjunction definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 681
diff changeset
183 UR : Functor B A
a5f2ca67e7c5 fix monad/adjunction definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 681
diff changeset
184 FR : Functor A B
a5f2ca67e7c5 fix monad/adjunction definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 681
diff changeset
185 ηR : NTrans A A identityFunctor ( UR ○ FR )
a5f2ca67e7c5 fix monad/adjunction definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 681
diff changeset
186 εR : NTrans B B ( FR ○ UR ) identityFunctor
a5f2ca67e7c5 fix monad/adjunction definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 681
diff changeset
187 μ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
188 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
189 T=UF : Monad.T M ≃ (UR ○ FR)
a5f2ca67e7c5 fix monad/adjunction definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 681
diff changeset
190 μ=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
191 -- η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
192 -- μ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
193
88
419923b149ca on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 87
diff changeset
194
350
c483374f542b try equalizer from limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 312
diff changeset
195 --
c483374f542b try equalizer from limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 312
diff changeset
196 -- e f
c483374f542b try equalizer from limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 312
diff changeset
197 -- c -------→ a ---------→ b
c483374f542b try equalizer from limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 312
diff changeset
198 -- ^ . ---------→
c483374f542b try equalizer from limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 312
diff changeset
199 -- | . g
c483374f542b try equalizer from limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 312
diff changeset
200 -- |k .
c483374f542b try equalizer from limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 312
diff changeset
201 -- | . h
c483374f542b try equalizer from limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 312
diff changeset
202 -- d
c483374f542b try equalizer from limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 312
diff changeset
203
443
f526f4b68565 fix IsEqualizer
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 440
diff changeset
204 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
205 field
a87d3ea9efe4 pullback
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 253
diff changeset
206 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
207 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
208 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
209 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
210 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
211 equalizer1 : Hom A c a
f526f4b68565 fix IsEqualizer
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 440
diff changeset
212 equalizer1 = e
260
a87d3ea9efe4 pullback
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 253
diff changeset
213
443
f526f4b68565 fix IsEqualizer
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 440
diff changeset
214 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
215 field
443
f526f4b68565 fix IsEqualizer
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 440
diff changeset
216 equalizer-c : Obj A
f526f4b68565 fix IsEqualizer
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 440
diff changeset
217 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
218 isEqualizer : IsEqualizer A equalizer f g
440
ff36c500962e fix limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 350
diff changeset
219
468
c375d8f93a2c discrete category and product from a limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 460
diff changeset
220 --
260
a87d3ea9efe4 pullback
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 253
diff changeset
221 -- Product
a87d3ea9efe4 pullback
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 253
diff changeset
222 --
264
78ce12f8e6b6 pullback done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 260
diff changeset
223 -- c
78ce12f8e6b6 pullback done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 260
diff changeset
224 -- f | g
78ce12f8e6b6 pullback done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 260
diff changeset
225 -- |f×g
78ce12f8e6b6 pullback done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 260
diff changeset
226 -- v
300
d6a6dd305da2 arrow and lambda fix
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 268
diff changeset
227 -- a <-------- ab ---------→ b
264
78ce12f8e6b6 pullback done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 260
diff changeset
228 -- π1 π2
260
a87d3ea9efe4 pullback
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 253
diff changeset
229
a87d3ea9efe4 pullback
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 253
diff changeset
230
672
749df4959d19 fix completeness
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 669
diff changeset
231 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
232 ( π1 : Hom A ab a )
a87d3ea9efe4 pullback
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 253
diff changeset
233 ( π2 : Hom A ab b )
a87d3ea9efe4 pullback
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 253
diff changeset
234 : Set (ℓ ⊔ (c₁ ⊔ c₂)) where
a87d3ea9efe4 pullback
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 253
diff changeset
235 field
a87d3ea9efe4 pullback
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 253
diff changeset
236 _×_ : {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
237 π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
238 π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
239 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
240 ×-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
241
681
bd8f7346f252 fix Product and pullback
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 676
diff changeset
242 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
243 : Set (ℓ ⊔ (c₁ ⊔ c₂)) where
ff36c500962e fix limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 350
diff changeset
244 field
681
bd8f7346f252 fix Product and pullback
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 676
diff changeset
245 product : Obj A
bd8f7346f252 fix Product and pullback
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 676
diff changeset
246 π1 : Hom A product a
bd8f7346f252 fix Product and pullback
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 676
diff changeset
247 π2 : Hom A product b
bd8f7346f252 fix Product and pullback
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 676
diff changeset
248 isProduct : IsProduct A a b product π1 π2
260
a87d3ea9efe4 pullback
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 253
diff changeset
249
468
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 --
c375d8f93a2c discrete category and product from a limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 460
diff changeset
252 -- product on arbitrary index
c375d8f93a2c discrete category and product from a limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 460
diff changeset
253 --
c375d8f93a2c discrete category and product from a limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 460
diff changeset
254
691
917e51be9bbf change argument of Limit and K
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 690
diff changeset
255 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
256 ( p : Obj A ) -- product
c375d8f93a2c discrete category and product from a limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 460
diff changeset
257 ( ai : I → Obj A ) -- families
508
3ce21b2a671a IProduct is written in Sets
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 495
diff changeset
258 ( 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
259 : 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
260 field
c375d8f93a2c discrete category and product from a limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 460
diff changeset
261 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
262 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
263 → ∀ { 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
264 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
265 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
266 → ( ∀ (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
267 -- another form of uniquness
c375d8f93a2c discrete category and product from a limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 460
diff changeset
268 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
269 → ( ∀ { 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
270 → A [ product' ≈ iproduct qi ]
c375d8f93a2c discrete category and product from a limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 460
diff changeset
271 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
272 product'
c375d8f93a2c discrete category and product from a limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 460
diff changeset
273 ≈↑⟨ ip-uniqueness ⟩
c375d8f93a2c discrete category and product from a limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 460
diff changeset
274 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
275 ≈⟨ ip-cong ( λ i → begin
c375d8f93a2c discrete category and product from a limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 460
diff changeset
276 pi i o product'
c375d8f93a2c discrete category and product from a limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 460
diff changeset
277 ≈⟨ eq {i} ⟩
c375d8f93a2c discrete category and product from a limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 460
diff changeset
278 qi i
c375d8f93a2c discrete category and product from a limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 460
diff changeset
279 ∎ ) ⟩
c375d8f93a2c discrete category and product from a limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 460
diff changeset
280 iproduct qi
c375d8f93a2c discrete category and product from a limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 460
diff changeset
281 ∎
c375d8f93a2c discrete category and product from a limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 460
diff changeset
282
691
917e51be9bbf change argument of Limit and K
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 690
diff changeset
283 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
284 field
3ce21b2a671a IProduct is written in Sets
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 495
diff changeset
285 iprod : Obj A
3ce21b2a671a IProduct is written in Sets
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 495
diff changeset
286 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
287 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
288
468
c375d8f93a2c discrete category and product from a limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 460
diff changeset
289
260
a87d3ea9efe4 pullback
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 253
diff changeset
290 -- Pullback
a87d3ea9efe4 pullback
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 253
diff changeset
291 -- f
300
d6a6dd305da2 arrow and lambda fix
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 268
diff changeset
292 -- a ------→ c
468
c375d8f93a2c discrete category and product from a limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 460
diff changeset
293 -- ^ ^
260
a87d3ea9efe4 pullback
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 253
diff changeset
294 -- π1 | |g
a87d3ea9efe4 pullback
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 253
diff changeset
295 -- | |
300
d6a6dd305da2 arrow and lambda fix
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 268
diff changeset
296 -- ab ------→ b
260
a87d3ea9efe4 pullback
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 253
diff changeset
297 -- ^ π2
a87d3ea9efe4 pullback
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 253
diff changeset
298 -- |
468
c375d8f93a2c discrete category and product from a limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 460
diff changeset
299 -- d
260
a87d3ea9efe4 pullback
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 253
diff changeset
300 --
681
bd8f7346f252 fix Product and pullback
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 676
diff changeset
301 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
302 ( f : Hom A a c ) ( g : Hom A b c )
a87d3ea9efe4 pullback
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 253
diff changeset
303 ( π1 : Hom A ab a ) ( π2 : Hom A ab b )
a87d3ea9efe4 pullback
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 253
diff changeset
304 : Set (ℓ ⊔ (c₁ ⊔ c₂)) where
a87d3ea9efe4 pullback
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 253
diff changeset
305 field
a87d3ea9efe4 pullback
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 253
diff changeset
306 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
307 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
308 π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
309 → 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
310 π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
311 → 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
312 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
313 → { π1p=π1' : A [ A [ π1 o p' ] ≈ π1' ] }
a87d3ea9efe4 pullback
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 253
diff changeset
314 → { π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
315 → A [ pullback eq ≈ p' ]
bd8f7346f252 fix Product and pullback
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 676
diff changeset
316
bd8f7346f252 fix Product and pullback
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 676
diff changeset
317 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
318 ( 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
319 : Set (ℓ ⊔ (c₁ ⊔ c₂)) where
bd8f7346f252 fix Product and pullback
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 676
diff changeset
320 field
bd8f7346f252 fix Product and pullback
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 676
diff changeset
321 ab : Obj A
bd8f7346f252 fix Product and pullback
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 676
diff changeset
322 π1 : Hom A ab a
bd8f7346f252 fix Product and pullback
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 676
diff changeset
323 π2 : Hom A ab b
bd8f7346f252 fix Product and pullback
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 676
diff changeset
324 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
325
702adc45704f is this right direction?
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 300
diff changeset
326 --
702adc45704f is this right direction?
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 300
diff changeset
327 -- Limit
702adc45704f is this right direction?
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 300
diff changeset
328 --
702adc45704f is this right direction?
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 300
diff changeset
329 -----
702adc45704f is this right direction?
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 300
diff changeset
330
702adc45704f is this right direction?
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 300
diff changeset
331 -- Constancy Functor
702adc45704f is this right direction?
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 300
diff changeset
332
691
917e51be9bbf change argument of Limit and K
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 690
diff changeset
333 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
334 → ( 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
335 K I A a = record {
312
702adc45704f is this right direction?
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 300
diff changeset
336 FObj = λ i → a ;
702adc45704f is this right direction?
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 300
diff changeset
337 FMap = λ f → id1 A a ;
702adc45704f is this right direction?
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 300
diff changeset
338 isFunctor = let open ≈-Reasoning (A) in record {
702adc45704f is this right direction?
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 300
diff changeset
339 ≈-cong = λ f=g → refl-hom
702adc45704f is this right direction?
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 300
diff changeset
340 ; identity = refl-hom
702adc45704f is this right direction?
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 300
diff changeset
341 ; distr = sym idL
702adc45704f is this right direction?
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 300
diff changeset
342 }
702adc45704f is this right direction?
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 300
diff changeset
343 }
702adc45704f is this right direction?
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 300
diff changeset
344
702adc45704f is this right direction?
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 300
diff changeset
345
691
917e51be9bbf change argument of Limit and K
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 690
diff changeset
346 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
347 (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
348 field
691
917e51be9bbf change argument of Limit and K
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 690
diff changeset
349 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
350 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
351 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
352 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
353 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
354
691
917e51be9bbf change argument of Limit and K
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 690
diff changeset
355 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
356 : Set (suc (c₁' ⊔ c₂' ⊔ ℓ' ⊔ c₁ ⊔ c₂ ⊔ ℓ )) where
c257347a27f3 found limit in freyd
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 484
diff changeset
357 field
c257347a27f3 found limit in freyd
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 484
diff changeset
358 a0 : Obj A
691
917e51be9bbf change argument of Limit and K
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 690
diff changeset
359 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
360 isLimit : IsLimit I A Γ a0 t0
487
c257347a27f3 found limit in freyd
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 484
diff changeset
361
691
917e51be9bbf change argument of Limit and K
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 690
diff changeset
362 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
363 ( C : Category c₁'' c₂'' ℓ'' )
c257347a27f3 found limit in freyd
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 484
diff changeset
364 ( Γ : Functor I B )
691
917e51be9bbf change argument of Limit and K
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 690
diff changeset
365 ( 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
366 ( 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
367 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
368 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
369 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
370 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
371 ≈⟨ 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
372 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
373 ≈⟨ 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
374 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
375 ∎
c257347a27f3 found limit in freyd
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 484
diff changeset
376 } }
c257347a27f3 found limit in freyd
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 484
diff changeset
377
c257347a27f3 found limit in freyd
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 484
diff changeset
378 open Limit
691
917e51be9bbf change argument of Limit and K
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 690
diff changeset
379 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
380 { c₁'' c₂'' ℓ'' : Level} ( C : Category c₁'' c₂'' ℓ'' )
c257347a27f3 found limit in freyd
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 484
diff changeset
381 (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
382 field
691
917e51be9bbf change argument of Limit and K
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 690
diff changeset
383 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
384 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
385 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
386 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
387 ; 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
388 ; isLimit = preserve Γ limita }
c257347a27f3 found limit in freyd
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 484
diff changeset
389
468
c375d8f93a2c discrete category and product from a limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 460
diff changeset
390 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
391 : Set (suc (c₁' ⊔ c₂' ⊔ ℓ' ⊔ c₁ ⊔ c₂ ⊔ ℓ )) where
ff36c500962e fix limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 350
diff changeset
392 field
691
917e51be9bbf change argument of Limit and K
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 690
diff changeset
393 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
394 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
395 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
396 open Limit
672
749df4959d19 fix completeness
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 669
diff changeset
397 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
398 limit-c Γ = a0 ( climit Γ)
691
917e51be9bbf change argument of Limit and K
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 690
diff changeset
399 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
400 limit-u Γ = t0 ( climit Γ)
672
749df4959d19 fix completeness
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 669
diff changeset
401 open Equalizer
749df4959d19 fix completeness
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 669
diff changeset
402 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
403 equalizer-p f g = equalizer-c (cequalizer f g )
749df4959d19 fix completeness
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 669
diff changeset
404 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
405 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
406
662
e1d54c0f73a7 move InitialObject to cat-utility
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 526
diff changeset
407
e1d54c0f73a7 move InitialObject to cat-utility
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 526
diff changeset
408 -- initial object
e1d54c0f73a7 move InitialObject to cat-utility
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 526
diff changeset
409
695
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 691
diff changeset
410 record HasInitialObject {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
411 field
e1d54c0f73a7 move InitialObject to cat-utility
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 526
diff changeset
412 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
413 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
414
688
a5f2ca67e7c5 fix monad/adjunction definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 681
diff changeset
415 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
416 field
a5f2ca67e7c5 fix monad/adjunction definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 681
diff changeset
417 initialObject : Obj A
695
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 691
diff changeset
418 hasInitialObject : HasInitialObject A initialObject
688
a5f2ca67e7c5 fix monad/adjunction definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 681
diff changeset
419