Mercurial > hg > Members > kono > Proof > category
annotate src/freyd2.agda @ 1115:5620d4a85069
safe rewriting nearly finished
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Wed, 03 Jul 2024 11:44:58 +0900 |
| parents | 0e750446e463 |
| children |
| rev | line source |
|---|---|
|
1110
45de2b31bf02
add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1107
diff
changeset
|
1 {-# OPTIONS --cubical-compatible --safe #-} |
|
45de2b31bf02
add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1107
diff
changeset
|
2 |
|
497
e8b85a05a6b2
add if U is iso to representable functor then preserve limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
3 open import Category -- https://github.com/konn/category-agda |
|
e8b85a05a6b2
add if U is iso to representable functor then preserve limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
4 open import Level |
| 1112 | 5 open import Category.Sets -- renaming ( _o_ to _*_ ) |
| 1111 | 6 open import Relation.Binary.Core |
| 7 open import Relation.Binary.PropositionalEquality hiding ( [_] ; sym ; resp ) | |
|
497
e8b85a05a6b2
add if U is iso to representable functor then preserve limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
8 |
| 1111 | 9 module freyd2 ( |
| 10 ≡←≈ : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) {a b : Obj A } { x y : Hom A a b } → (x≈y : A [ x ≈ y ]) → x ≡ y ) | |
|
497
e8b85a05a6b2
add if U is iso to representable functor then preserve limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
11 where |
|
e8b85a05a6b2
add if U is iso to representable functor then preserve limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
12 |
|
e8b85a05a6b2
add if U is iso to representable functor then preserve limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
13 open import HomReasoning |
|
1110
45de2b31bf02
add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1107
diff
changeset
|
14 open import Definitions |
|
497
e8b85a05a6b2
add if U is iso to representable functor then preserve limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
15 open import Function |
|
e8b85a05a6b2
add if U is iso to representable functor then preserve limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
16 |
|
e8b85a05a6b2
add if U is iso to representable functor then preserve limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
17 ---------- |
|
e8b85a05a6b2
add if U is iso to representable functor then preserve limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
18 -- |
| 693 | 19 -- A is locally small complete and K{*}↓U has preinitial full subcategory, U is an adjoint functor |
| 20 -- | |
|
497
e8b85a05a6b2
add if U is iso to representable functor then preserve limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
21 -- a : Obj A |
|
e8b85a05a6b2
add if U is iso to representable functor then preserve limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
22 -- U : A → Sets |
|
e8b85a05a6b2
add if U is iso to representable functor then preserve limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
23 -- U ⋍ Hom (a,-) |
|
e8b85a05a6b2
add if U is iso to representable functor then preserve limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
24 -- |
|
e8b85a05a6b2
add if U is iso to representable functor then preserve limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
25 |
| 781 | 26 |
| 693 | 27 -- A is localy small |
|
497
e8b85a05a6b2
add if U is iso to representable functor then preserve limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
28 |
|
949
ac53803b3b2a
reorganization for apkg
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
781
diff
changeset
|
29 import Axiom.Extensionality.Propositional |
|
497
e8b85a05a6b2
add if U is iso to representable functor then preserve limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
30 -- Extensionality a b = {A : Set a} {B : A → Set b} {f g : (x : A) → B x} → (∀ x → f x ≡ g x) → f ≡ g → ( λ x → f x ≡ λ x → g x ) |
| 1034 | 31 -- postulate extensionality : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) → Axiom.Extensionality.Propositional.Extensionality c₂ c₂ |
|
497
e8b85a05a6b2
add if U is iso to representable functor then preserve limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
32 |
|
e8b85a05a6b2
add if U is iso to representable functor then preserve limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
33 ---- |
|
e8b85a05a6b2
add if U is iso to representable functor then preserve limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
34 -- |
|
617
34540494fdcf
initital obj uniquness done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
616
diff
changeset
|
35 -- Hom ( a, - ) is Object mapping in Yoneda Functor |
|
497
e8b85a05a6b2
add if U is iso to representable functor then preserve limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
36 -- |
|
e8b85a05a6b2
add if U is iso to representable functor then preserve limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
37 ---- |
|
e8b85a05a6b2
add if U is iso to representable functor then preserve limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
38 |
|
e8b85a05a6b2
add if U is iso to representable functor then preserve limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
39 open NTrans |
|
e8b85a05a6b2
add if U is iso to representable functor then preserve limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
40 open Functor |
|
498
c981a2f0642f
UpreseveLimit detailing
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
497
diff
changeset
|
41 open Limit |
|
c981a2f0642f
UpreseveLimit detailing
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
497
diff
changeset
|
42 open IsLimit |
|
c981a2f0642f
UpreseveLimit detailing
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
497
diff
changeset
|
43 open import Category.Cat |
|
497
e8b85a05a6b2
add if U is iso to representable functor then preserve limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
44 |
| 609 | 45 open Representable |
| 502 | 46 |
|
624
9b9bc1e076f3
introduce one element set
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
623
diff
changeset
|
47 _↓_ : { c₁ c₂ ℓ : Level} { c₁' c₂' ℓ' : Level} { A : Category c₁ c₂ ℓ } { B : Category c₁' c₂' ℓ' } |
|
9b9bc1e076f3
introduce one element set
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
623
diff
changeset
|
48 → ( F G : Functor A B ) |
|
9b9bc1e076f3
introduce one element set
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
623
diff
changeset
|
49 → Category (c₂' ⊔ c₁) (ℓ' ⊔ c₂) ℓ |
|
9b9bc1e076f3
introduce one element set
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
623
diff
changeset
|
50 _↓_ { c₁} {c₂} {ℓ} {c₁'} {c₂'} {ℓ'} { A } { B } F G = CommaCategory |
|
9b9bc1e076f3
introduce one element set
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
623
diff
changeset
|
51 where open import Comma1 F G |
|
9b9bc1e076f3
introduce one element set
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
623
diff
changeset
|
52 |
|
9b9bc1e076f3
introduce one element set
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
623
diff
changeset
|
53 open Complete |
| 695 | 54 open HasInitialObject |
|
624
9b9bc1e076f3
introduce one element set
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
623
diff
changeset
|
55 open import Comma1 |
|
9b9bc1e076f3
introduce one element set
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
623
diff
changeset
|
56 open CommaObj |
| 609 | 57 open LimitPreserve |
| 608 | 58 |
| 609 | 59 -- Representable Functor U preserve limit , so K{*}↓U is complete |
| 610 | 60 -- |
| 616 | 61 -- Yoneda A b = λ a → Hom A a b : Functor A Sets |
|
617
34540494fdcf
initital obj uniquness done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
616
diff
changeset
|
62 -- : Functor Sets A |
| 610 | 63 |
|
635
f7cc0ec00e05
introduce U preserving
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
634
diff
changeset
|
64 YonedaFpreserveLimit0 : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (I : Category c₁ c₂ ℓ) |
| 612 | 65 (b : Obj A ) |
| 1106 | 66 (Γ : Functor I (Category.op A)) (limita : Limit I (Category.op A) Γ) → |
| 67 IsLimit I Sets (Yoneda A (≡←≈ A) b ○ Γ) (FObj (Yoneda A (≡←≈ A) b) (a0 limita)) (LimitNat I (Category.op A) Sets Γ (a0 limita) (t0 limita) (Yoneda A (≡←≈ A) b)) | |
|
635
f7cc0ec00e05
introduce U preserving
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
634
diff
changeset
|
68 YonedaFpreserveLimit0 {c₁} {c₂} {ℓ} A I b Γ lim = record { |
|
611
b1b5c6b4c570
natural transformation in representable functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
610
diff
changeset
|
69 limit = λ a t → ψ a t |
|
b1b5c6b4c570
natural transformation in representable functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
610
diff
changeset
|
70 ; t0f=t = λ {a t i} → t0f=t0 a t i |
|
614
e6be03d94284
Representational Functor preserve limit done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
613
diff
changeset
|
71 ; limit-uniqueness = λ {b} {t} {f} t0f=t → limit-uniqueness0 {b} {t} {f} t0f=t |
| 610 | 72 } where |
| 1106 | 73 opA = Category.op A |
| 74 hat0 : NTrans I Sets (K I Sets (FObj (Yoneda A (≡←≈ A) b) (a0 lim))) (Yoneda A (≡←≈ A) b ○ Γ) | |
| 75 hat0 = LimitNat I opA Sets Γ (a0 lim) (t0 lim) (Yoneda A (≡←≈ A) b) | |
|
611
b1b5c6b4c570
natural transformation in representable functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
610
diff
changeset
|
76 haa0 : Obj Sets |
| 1106 | 77 haa0 = FObj (Yoneda A (≡←≈ A) b) (a0 lim) |
| 1111 | 78 _*_ : {a b c : Obj (Sets {c₁} ) } → (b → c) → (a → b) → a → c |
| 79 _*_ f g = λ x → f (g x) | |
| 1106 | 80 ta : (a : Obj Sets) ( x : a ) ( t : NTrans I Sets (K I Sets a) (Yoneda A (≡←≈ A) b ○ Γ)) → NTrans I opA (K I opA b ) Γ |
|
611
b1b5c6b4c570
natural transformation in representable functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
610
diff
changeset
|
81 ta a x t = record { TMap = λ i → (TMap t i ) x ; isNTrans = record { commute = commute1 } } where |
|
b1b5c6b4c570
natural transformation in representable functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
610
diff
changeset
|
82 commute1 : {a₁ b₁ : Obj I} {f : Hom I a₁ b₁} → |
| 1106 | 83 opA [ opA [ FMap Γ f o TMap t a₁ x ] ≈ opA [ TMap t b₁ x o FMap (K I opA b) f ] ] |
| 84 commute1 {a₁} {b₁} {f} = let open ≈-Reasoning opA in begin | |
| 1111 | 85 opA [ FMap Γ f o TMap t a₁ x ] ≈⟨ ≈←≡ (IsNTrans.commute (isNTrans t) x ) ⟩ |
| 86 (Sets [ TMap t b₁ o id1 Sets a ]) x ≈⟨⟩ | |
| 87 TMap t b₁ x ≈⟨ sym idR ⟩ | |
| 88 opA [ TMap t b₁ x o id1 opA b ] ∎ | |
| 1106 | 89 ψ : (X : Obj Sets) ( t : NTrans I Sets (K I Sets X) (Yoneda A (≡←≈ A) b ○ Γ)) |
| 90 → Hom Sets X (FObj (Yoneda A (≡←≈ A) b) (a0 lim)) | |
| 91 ψ X t x = FMap (Yoneda A (≡←≈ A) b) (limit (isLimit lim) b (ta X x t )) (id1 A b ) | |
| 92 t0f=t0 : (a : Obj Sets ) ( t : NTrans I Sets (K I Sets a) (Yoneda A (≡←≈ A) b ○ Γ)) (i : Obj I) | |
| 93 → Sets [ Sets [ TMap (LimitNat I opA Sets Γ (a0 lim) (t0 lim) (Yoneda A (≡←≈ A) b)) i o ψ a t ] ≈ TMap t i ] | |
| 1111 | 94 t0f=t0 a t i = let open ≈-Reasoning opA in ( λ x → (≡←≈ A) ( begin |
| 1106 | 95 ( Sets [ TMap (LimitNat I opA Sets Γ (a0 lim) (t0 lim) (Yoneda A (≡←≈ A) b)) i o ψ a t ] ) x |
| 612 | 96 ≈⟨⟩ |
| 1106 | 97 FMap (Yoneda A (≡←≈ A) b) ( TMap (t0 lim) i) (FMap (Yoneda A (≡←≈ A) b) (limit (isLimit lim) b (ta a x t )) (id1 A b )) |
|
615
a45c32ceca97
initial Object's arrow found
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
614
diff
changeset
|
98 ≈⟨⟩ -- FMap (Hom A b ) f g = A [ f o g ] |
| 613 | 99 TMap (t0 lim) i o (limit (isLimit lim) b (ta a x t ) o id1 A b ) |
| 100 ≈⟨ cdr idR ⟩ | |
| 101 TMap (t0 lim) i o limit (isLimit lim) b (ta a x t ) | |
| 102 ≈⟨ t0f=t (isLimit lim) ⟩ | |
| 103 TMap (ta a x t) i | |
| 104 ≈⟨⟩ | |
| 612 | 105 TMap t i x |
| 106 ∎ )) | |
| 1106 | 107 limit-uniqueness0 : {a : Obj Sets} {t : NTrans I Sets (K I Sets a) (Yoneda A (≡←≈ A) b ○ Γ)} {f : Hom Sets a (FObj (Yoneda A (≡←≈ A) b) (a0 lim))} → |
| 108 ({i : Obj I} → Sets [ Sets [ TMap (LimitNat I opA Sets Γ (a0 lim) (t0 lim) (Yoneda A (≡←≈ A) b)) i o f ] ≈ TMap t i ]) → | |
|
614
e6be03d94284
Representational Functor preserve limit done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
613
diff
changeset
|
109 Sets [ ψ a t ≈ f ] |
| 1111 | 110 limit-uniqueness0 {a} {t} {f} t0f=t = let open ≈-Reasoning opA in ( λ x → (≡←≈ A) ( begin |
|
614
e6be03d94284
Representational Functor preserve limit done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
613
diff
changeset
|
111 ψ a t x |
|
e6be03d94284
Representational Functor preserve limit done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
613
diff
changeset
|
112 ≈⟨⟩ |
| 1106 | 113 FMap (Yoneda A (≡←≈ A) b) (limit (isLimit lim) b (ta a x t )) (id1 A b ) |
|
614
e6be03d94284
Representational Functor preserve limit done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
613
diff
changeset
|
114 ≈⟨⟩ |
|
e6be03d94284
Representational Functor preserve limit done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
613
diff
changeset
|
115 limit (isLimit lim) b (ta a x t ) o id1 A b |
|
e6be03d94284
Representational Functor preserve limit done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
613
diff
changeset
|
116 ≈⟨ idR ⟩ |
|
e6be03d94284
Representational Functor preserve limit done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
613
diff
changeset
|
117 limit (isLimit lim) b (ta a x t ) |
| 1112 | 118 ≈⟨ limit-uniqueness (isLimit lim) ( λ {i} → ≈←≡ ( t0f=t {i} x )) ⟩ |
|
614
e6be03d94284
Representational Functor preserve limit done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
613
diff
changeset
|
119 f x |
|
e6be03d94284
Representational Functor preserve limit done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
613
diff
changeset
|
120 ∎ )) |
| 610 | 121 |
| 609 | 122 |
|
691
917e51be9bbf
change argument of Limit and K
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
690
diff
changeset
|
123 YonedaFpreserveLimit : {c₁ c₂ ℓ : Level} (I : Category c₁ c₂ ℓ) (A : Category c₁ c₂ ℓ) |
| 1106 | 124 (b : Obj A ) → LimitPreserve I (Category.op A) Sets (Yoneda A (≡←≈ A) b) |
| 125 YonedaFpreserveLimit I opA b = record { | |
| 126 preserve = λ Γ lim → YonedaFpreserveLimit0 opA I b Γ lim | |
| 610 | 127 } |
| 609 | 128 |
|
624
9b9bc1e076f3
introduce one element set
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
623
diff
changeset
|
129 |
| 608 | 130 -- K{*}↓U has preinitial full subcategory if U is representable |
| 609 | 131 -- if U is representable, K{*}↓U has initial Object ( so it has preinitial full subcategory ) |
| 608 | 132 |
|
617
34540494fdcf
initital obj uniquness done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
616
diff
changeset
|
133 open CommaHom |
|
34540494fdcf
initital obj uniquness done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
616
diff
changeset
|
134 |
| 627 | 135 data * {c : Level} : Set c where |
| 136 OneObj : * | |
| 137 | |
| 609 | 138 KUhasInitialObj : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) |
| 608 | 139 (a : Obj A ) |
| 1106 | 140 → HasInitialObject ( K (Category.op A) Sets * ↓ (Yoneda A (≡←≈ A) a) ) ( record { obj = a ; hom = λ x → id1 A a } ) |
| 621 | 141 KUhasInitialObj {c₁} {c₂} {ℓ} A a = record { |
|
615
a45c32ceca97
initial Object's arrow found
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
614
diff
changeset
|
142 initial = λ b → initial0 b |
| 636 | 143 ; uniqueness = λ f → unique f |
|
615
a45c32ceca97
initial Object's arrow found
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
614
diff
changeset
|
144 } where |
| 1106 | 145 opA = Category.op A |
| 621 | 146 commaCat : Category (c₂ ⊔ c₁) c₂ ℓ |
| 1106 | 147 commaCat = K opA Sets * ↓ Yoneda A (≡←≈ A) a |
| 148 initObj : Obj (K opA Sets * ↓ Yoneda A (≡←≈ A) a) | |
|
624
9b9bc1e076f3
introduce one element set
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
623
diff
changeset
|
149 initObj = record { obj = a ; hom = λ x → id1 A a } |
| 1106 | 150 comm2 : (b : Obj commaCat) ( x : * ) → ( Sets [ FMap (Yoneda A (≡←≈ A) a) (hom b OneObj) o (λ x₁ → id1 A a) ] ) x ≡ hom b x |
| 151 comm2 b OneObj = let open ≈-Reasoning opA in (≡←≈ A) ( begin | |
| 152 ( Sets [ FMap (Yoneda A (≡←≈ A) a) (hom b OneObj) o (λ x₁ → id1 A a) ] ) OneObj | |
|
624
9b9bc1e076f3
introduce one element set
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
623
diff
changeset
|
153 ≈⟨⟩ |
| 1106 | 154 FMap (Yoneda A (≡←≈ A) a) (hom b OneObj) (id1 A a) |
|
624
9b9bc1e076f3
introduce one element set
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
623
diff
changeset
|
155 ≈⟨⟩ |
|
9b9bc1e076f3
introduce one element set
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
623
diff
changeset
|
156 hom b OneObj o id1 A a |
|
9b9bc1e076f3
introduce one element set
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
623
diff
changeset
|
157 ≈⟨ idR ⟩ |
|
9b9bc1e076f3
introduce one element set
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
623
diff
changeset
|
158 hom b OneObj |
|
9b9bc1e076f3
introduce one element set
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
623
diff
changeset
|
159 ∎ ) |
| 1106 | 160 comm1 : (b : Obj commaCat) → Sets [ Sets [ FMap (Yoneda A (≡←≈ A) a) (hom b OneObj) o hom initObj ] ≈ Sets [ hom b o FMap (K opA Sets *) (hom b OneObj) ] ] |
|
624
9b9bc1e076f3
introduce one element set
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
623
diff
changeset
|
161 comm1 b = let open ≈-Reasoning Sets in begin |
| 1106 | 162 FMap (Yoneda A (≡←≈ A) a) (hom b OneObj) o ( λ x → id1 A a ) |
| 1111 | 163 ≈⟨ ( λ x → comm2 b x ) ⟩ |
|
624
9b9bc1e076f3
introduce one element set
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
623
diff
changeset
|
164 hom b |
|
615
a45c32ceca97
initial Object's arrow found
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
614
diff
changeset
|
165 ≈⟨⟩ |
| 1106 | 166 hom b o FMap (K opA Sets *) (hom b OneObj) |
|
615
a45c32ceca97
initial Object's arrow found
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
614
diff
changeset
|
167 ∎ |
|
624
9b9bc1e076f3
introduce one element set
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
623
diff
changeset
|
168 initial0 : (b : Obj commaCat) → |
|
9b9bc1e076f3
introduce one element set
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
623
diff
changeset
|
169 Hom commaCat initObj b |
|
615
a45c32ceca97
initial Object's arrow found
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
614
diff
changeset
|
170 initial0 b = record { |
|
624
9b9bc1e076f3
introduce one element set
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
623
diff
changeset
|
171 arrow = hom b OneObj |
|
9b9bc1e076f3
introduce one element set
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
623
diff
changeset
|
172 ; comm = comm1 b } |
| 625 | 173 -- what is comm f ? |
| 1106 | 174 comm-f : (b : Obj (K opA Sets * ↓ (Yoneda A (≡←≈ A) a))) (f : Hom (K opA Sets * ↓ Yoneda A (≡←≈ A) a) initObj b) |
| 175 → Sets [ Sets [ FMap (Yoneda A (≡←≈ A) a) (arrow f) o ( λ x → id1 A a ) ] | |
| 176 ≈ Sets [ hom b o FMap (K opA Sets *) (arrow f) ] ] | |
| 625 | 177 comm-f b f = comm f |
| 1106 | 178 unique : {b : Obj (K opA Sets * ↓ Yoneda A (≡←≈ A) a)} (f : Hom (K opA Sets * ↓ Yoneda A (≡←≈ A) a) initObj b) |
| 179 → (K opA Sets * ↓ Yoneda A (≡←≈ A) a) [ f ≈ initial0 b ] | |
| 180 unique {b} f = let open ≈-Reasoning opA in begin | |
|
624
9b9bc1e076f3
introduce one element set
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
623
diff
changeset
|
181 arrow f |
|
9b9bc1e076f3
introduce one element set
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
623
diff
changeset
|
182 ≈↑⟨ idR ⟩ |
|
9b9bc1e076f3
introduce one element set
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
623
diff
changeset
|
183 arrow f o id1 A a |
|
9b9bc1e076f3
introduce one element set
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
623
diff
changeset
|
184 ≈⟨⟩ |
| 1106 | 185 ( Sets [ FMap (Yoneda A (≡←≈ A) a) (arrow f) o id1 Sets (FObj (Yoneda A (≡←≈ A) a) a) ] ) (id1 A a) |
| 625 | 186 ≈⟨⟩ |
| 1106 | 187 ( Sets [ FMap (Yoneda A (≡←≈ A) a) (arrow f) o ( λ x → id1 A a ) ] ) OneObj |
| 1111 | 188 ≈⟨ ≈←≡ ( comm f OneObj ) ⟩ |
| 1106 | 189 ( Sets [ hom b o FMap (K opA Sets *) (arrow f) ] ) OneObj |
|
624
9b9bc1e076f3
introduce one element set
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
623
diff
changeset
|
190 ≈⟨⟩ |
|
9b9bc1e076f3
introduce one element set
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
623
diff
changeset
|
191 hom b OneObj |
|
9b9bc1e076f3
introduce one element set
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
623
diff
changeset
|
192 ∎ |
|
9b9bc1e076f3
introduce one element set
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
623
diff
changeset
|
193 |
|
615
a45c32ceca97
initial Object's arrow found
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
614
diff
changeset
|
194 |
|
a45c32ceca97
initial Object's arrow found
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
614
diff
changeset
|
195 |
|
644
8e35703ef116
representability theorem done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
643
diff
changeset
|
196 -- A is complete and K{*}↓U has preinitial full subcategory and U preserve limit then U is representable |
|
615
a45c32ceca97
initial Object's arrow found
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
614
diff
changeset
|
197 |
| 638 | 198 -- if U preserve limit, K{*}↓U has initial object from freyd.agda |
| 199 | |
| 626 | 200 ≡-cong = Relation.Binary.PropositionalEquality.cong |
| 201 | |
| 638 | 202 |
| 203 ub : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (U : Functor A (Sets {c₂}) )(b : Obj A) (x : FObj U b ) | |
|
691
917e51be9bbf
change argument of Limit and K
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
690
diff
changeset
|
204 → Hom Sets (FObj (K A Sets *) b) (FObj U b) |
| 638 | 205 ub A U b x OneObj = x |
| 206 ob : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (U : Functor A (Sets {c₂}) )(b : Obj A) (x : FObj U b ) | |
|
691
917e51be9bbf
change argument of Limit and K
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
690
diff
changeset
|
207 → Obj ( K A Sets * ↓ U) |
| 638 | 208 ob A U b x = record { obj = b ; hom = ub A U b x} |
| 209 fArrow : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (U : Functor A (Sets {c₂}) ) {a b : Obj A} (f : Hom A a b) (x : FObj U a ) | |
|
691
917e51be9bbf
change argument of Limit and K
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
690
diff
changeset
|
210 → Hom ( K A Sets * ↓ U) ( ob A U a x ) (ob A U b (FMap U f x) ) |
| 638 | 211 fArrow A U {a} {b} f x = record { arrow = f ; comm = fArrowComm a b f x } |
| 212 where | |
| 213 fArrowComm1 : (a b : Obj A) (f : Hom A a b) (x : FObj U a ) → (y : * ) → FMap U f ( ub A U a x y ) ≡ ub A U b (FMap U f x) y | |
| 214 fArrowComm1 a b f x OneObj = refl | |
| 215 fArrowComm : (a b : Obj A) (f : Hom A a b) (x : FObj U a ) → | |
|
691
917e51be9bbf
change argument of Limit and K
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
690
diff
changeset
|
216 Sets [ Sets [ FMap U f o hom (ob A U a x) ] ≈ Sets [ hom (ob A U b (FMap U f x)) o FMap (K A Sets *) f ] ] |
| 1111 | 217 fArrowComm a b f x = ( λ y → begin |
| 638 | 218 ( Sets [ FMap U f o hom (ob A U a x) ] ) y |
| 219 ≡⟨⟩ | |
| 220 FMap U f ( hom (ob A U a x) y ) | |
| 221 ≡⟨⟩ | |
| 222 FMap U f ( ub A U a x y ) | |
| 223 ≡⟨ fArrowComm1 a b f x y ⟩ | |
| 224 ub A U b (FMap U f x) y | |
| 225 ≡⟨⟩ | |
| 226 hom (ob A U b (FMap U f x)) y | |
| 227 ∎ ) where | |
| 228 open import Relation.Binary.PropositionalEquality | |
| 229 open ≡-Reasoning | |
| 230 | |
|
635
f7cc0ec00e05
introduce U preserving
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
634
diff
changeset
|
231 |
|
f7cc0ec00e05
introduce U preserving
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
634
diff
changeset
|
232 -- if K{*}↓U has initial Obj, U is representable |
|
f7cc0ec00e05
introduce U preserving
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
634
diff
changeset
|
233 |
| 636 | 234 UisRepresentable : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) |
| 1106 | 235 (U : Functor (Category.op A) (Sets {c₂}) ) |
| 236 ( i : Obj ( K (Category.op A) Sets * ↓ U) ) | |
| 237 (In : HasInitialObject ( K (Category.op A) Sets * ↓ U) i ) | |
| 238 → Representable A (≡←≈ A) U (obj i) | |
| 636 | 239 UisRepresentable A U i In = record { |
| 627 | 240 repr→ = record { TMap = tmap1 ; isNTrans = record { commute = comm1 } } |
| 626 | 241 ; repr← = record { TMap = tmap2 ; isNTrans = record { commute = comm2 } } |
| 638 | 242 ; reprId→ = iso→ |
| 243 ; reprId← = iso← | |
| 626 | 244 } where |
| 1106 | 245 opA = Category.op A |
| 246 comm11 : (a b : Obj opA) (f : Hom opA a b) (y : FObj U a ) → | |
| 247 ( Sets [ FMap (Yoneda A (≡←≈ A) (obj i)) f o ( λ x → arrow (initial In (ob opA U a x))) ] ) y | |
| 248 ≡ (Sets [ ( λ x → arrow (initial In (ob opA U b x))) o FMap U f ] ) y | |
| 638 | 249 comm11 a b f y = begin |
| 1106 | 250 ( Sets [ FMap (Yoneda A (≡←≈ A) (obj i)) f o ( λ x → arrow (initial In (ob opA U a x))) ] ) y |
| 631 | 251 ≡⟨⟩ |
| 1106 | 252 opA [ f o arrow (initial In (ob opA U a y)) ] |
| 631 | 253 ≡⟨⟩ |
| 1106 | 254 opA [ arrow ( fArrow opA U f y ) o arrow (initial In (ob opA U a y)) ] |
| 255 ≡⟨ (≡←≈ A) ( uniqueness In {ob opA U b (FMap U f y) } (( K opA Sets * ↓ U) [ fArrow opA U f y o initial In (ob opA U a y)] ) ) ⟩ | |
| 256 arrow (initial In (ob opA U b (FMap U f y) )) | |
| 629 | 257 ≡⟨⟩ |
| 1106 | 258 (Sets [ ( λ x → arrow (initial In (ob opA U b x))) o FMap U f ] ) y |
| 629 | 259 ∎ where |
| 260 open import Relation.Binary.PropositionalEquality | |
| 261 open ≡-Reasoning | |
| 1106 | 262 tmap1 : (b : Obj A) → Hom Sets (FObj U b) (FObj (Yoneda A (≡←≈ A) (obj i)) b) |
| 263 tmap1 b x = arrow ( initial In (ob opA U b x ) ) | |
| 264 comm1 : {a b : Obj opA} {f : Hom opA a b} → Sets [ Sets [ FMap (Yoneda A (≡←≈ A) (obj i)) f o tmap1 a ] ≈ Sets [ tmap1 b o FMap U f ] ] | |
| 626 | 265 comm1 {a} {b} {f} = let open ≈-Reasoning Sets in begin |
| 1106 | 266 FMap (Yoneda A (≡←≈ A) (obj i)) f o tmap1 a |
| 629 | 267 ≈⟨⟩ |
| 1106 | 268 FMap (Yoneda A (≡←≈ A) (obj i)) f o ( λ x → arrow (initial In ( ob opA U a x ))) |
| 1111 | 269 ≈⟨ ( λ y → comm11 a b f y ) ⟩ |
| 1106 | 270 ( λ x → arrow (initial In (ob opA U b x))) o FMap U f |
| 629 | 271 ≈⟨⟩ |
| 626 | 272 tmap1 b o FMap U f |
| 273 ∎ | |
| 1106 | 274 comm21 : (a b : Obj opA) (f : Hom opA a b) ( y : Hom opA (obj i) a ) → |
| 636 | 275 (Sets [ FMap U f o (λ x → FMap U x (hom i OneObj))] ) y ≡ |
| 1106 | 276 (Sets [ ( λ x → (FMap U x ) (hom i OneObj)) o (λ x → opA [ f o x ] ) ] ) y |
| 626 | 277 comm21 a b f y = begin |
| 636 | 278 FMap U f ( FMap U y (hom i OneObj)) |
| 1111 | 279 ≡⟨ sym ( IsFunctor.distr (isFunctor U ) (hom i OneObj) ) ⟩ |
| 1106 | 280 (FMap U (opA [ f o y ] ) ) (hom i OneObj) |
| 626 | 281 ∎ where |
| 282 open import Relation.Binary.PropositionalEquality | |
| 283 open ≡-Reasoning | |
| 1106 | 284 tmap2 : (b : Obj A) → Hom Sets (FObj (Yoneda A (≡←≈ A) (obj i)) b) (FObj U b) |
| 636 | 285 tmap2 b x = ( FMap U x ) ( hom i OneObj ) |
| 1106 | 286 comm2 : {a b : Obj opA} {f : Hom opA a b} → Sets [ Sets [ FMap U f o tmap2 a ] ≈ |
| 287 Sets [ tmap2 b o FMap (Yoneda A (≡←≈ A) (obj i)) f ] ] | |
| 626 | 288 comm2 {a} {b} {f} = let open ≈-Reasoning Sets in begin |
| 289 FMap U f o tmap2 a | |
| 290 ≈⟨⟩ | |
| 636 | 291 FMap U f o ( λ x → ( FMap U x ) ( hom i OneObj ) ) |
| 1111 | 292 ≈⟨ ( λ y → comm21 a b f y ) ⟩ |
| 1106 | 293 ( λ x → ( FMap U x ) ( hom i OneObj ) ) o ( λ x → opA [ f o x ] ) |
| 636 | 294 ≈⟨⟩ |
| 1106 | 295 ( λ x → ( FMap U x ) ( hom i OneObj ) ) o FMap (Yoneda A (≡←≈ A) (obj i)) f |
| 636 | 296 ≈⟨⟩ |
| 1106 | 297 tmap2 b o FMap (Yoneda A (≡←≈ A) (obj i)) f |
|
637
946ea019a2e7
if K{*}↓U has initial Obj, U is representable done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
636
diff
changeset
|
298 ∎ |
| 1106 | 299 iso0 : ( x : Obj opA) ( y : Hom opA (obj i ) x ) ( z : * ) |
| 300 → ( Sets [ FMap U y o hom i ] ) z ≡ ( Sets [ ub opA U x (FMap U y (hom i OneObj)) o FMap (K opA Sets *) y ] ) z | |
|
637
946ea019a2e7
if K{*}↓U has initial Obj, U is representable done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
636
diff
changeset
|
301 iso0 x y OneObj = refl |
| 1106 | 302 iso→ : {x : Obj opA} → Sets [ Sets [ tmap1 x o tmap2 x ] ≈ id1 Sets (FObj (Yoneda A (≡←≈ A) (obj i)) x) ] |
| 1111 | 303 iso→ {x} = let open ≈-Reasoning opA in ( λ ( y : Hom opA (obj i ) x ) → (≡←≈ A) ( begin |
| 636 | 304 ( Sets [ tmap1 x o tmap2 x ] ) y |
| 626 | 305 ≈⟨⟩ |
| 1106 | 306 arrow ( initial In (ob opA U x (( FMap U y ) ( hom i OneObj ) ))) |
| 1111 | 307 ≈↑⟨ uniqueness In (record { arrow = y ; comm = ( λ (z : * ) → iso0 x y z ) } ) ⟩ |
| 636 | 308 y |
| 309 ∎ )) | |
| 310 iso← : {x : Obj A} → Sets [ Sets [ tmap2 x o tmap1 x ] ≈ id1 Sets (FObj U x) ] | |
| 1111 | 311 iso← {x} = ( λ (y : FObj U x ) → ( begin |
| 636 | 312 ( Sets [ tmap2 x o tmap1 x ] ) y |
| 313 ≡⟨⟩ | |
| 1106 | 314 ( FMap U ( arrow ( initial In (ob opA U x y ) )) ) ( hom i OneObj ) |
| 1111 | 315 ≡⟨ comm ( initial In (ob opA U x y ) ) OneObj ⟩ |
| 1106 | 316 hom (ob opA U x y) OneObj |
|
637
946ea019a2e7
if K{*}↓U has initial Obj, U is representable done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
636
diff
changeset
|
317 ≡⟨⟩ |
| 636 | 318 y |
| 319 ∎ ) ) where | |
| 320 open import Relation.Binary.PropositionalEquality | |
| 321 open ≡-Reasoning | |
| 645 | 322 |
| 647 | 323 ------------- |
| 324 -- Adjoint Functor Theorem | |
| 325 -- | |
| 326 | |
|
1115
5620d4a85069
safe rewriting nearly finished
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1112
diff
changeset
|
327 module Adjoint-Functor {c₁ c₂ ℓ : Level} (A B : Category c₁ c₂ ℓ) (I : Category c₁ c₂ ℓ) ( comp : Complete {c₁} {c₂} {ℓ} A ) |
| 648 | 328 (U : Functor A B ) |
|
691
917e51be9bbf
change argument of Limit and K
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
690
diff
changeset
|
329 (i : (b : Obj B) → Obj ( K A B b ↓ U) ) |
| 695 | 330 (In : (b : Obj B) → HasInitialObject ( K A B b ↓ U) (i b) ) |
|
663
855e497a9c8f
introducd HeterogeneousEquality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
662
diff
changeset
|
331 where |
| 648 | 332 |
| 649 | 333 tmap-η : (y : Obj B) → Hom B y (FObj U (obj (i y))) |
| 334 tmap-η y = hom (i y) | |
| 648 | 335 |
|
691
917e51be9bbf
change argument of Limit and K
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
690
diff
changeset
|
336 sobj : {a : Obj B} {b : Obj A} → ( f : Hom B a (FObj U b) ) → CommaObj (K A B a) U |
| 652 | 337 sobj {a} {b} f = record {obj = b; hom = f } |
|
691
917e51be9bbf
change argument of Limit and K
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
690
diff
changeset
|
338 solution : {a : Obj B} {b : Obj A} → ( f : Hom B a (FObj U b) ) → CommaHom (K A B a) U (i a) (sobj f) |
| 652 | 339 solution {a} {b} f = initial (In a) (sobj f) |
| 647 | 340 |
|
691
917e51be9bbf
change argument of Limit and K
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
690
diff
changeset
|
341 ηf : (a b : Obj B) → ( f : Hom B a b ) → Obj ( K A B a ↓ U) |
| 654 | 342 ηf a b f = sobj ( B [ tmap-η b o f ] ) |
| 343 | |
| 653 | 344 univ : {a : Obj B} {b : Obj A} → (f : Hom B a (FObj U b)) |
| 652 | 345 → B [ B [ FMap U (arrow (solution f)) o tmap-η a ] ≈ f ] |
| 653 | 346 univ {a} {b} f = let open ≈-Reasoning B in begin |
| 347 FMap U (arrow (solution f)) o tmap-η a | |
| 348 ≈⟨ comm (initial (In a) (sobj f)) ⟩ | |
|
691
917e51be9bbf
change argument of Limit and K
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
690
diff
changeset
|
349 hom (sobj f) o FMap (K A B a) (arrow (initial (In a) (sobj f))) |
| 653 | 350 ≈⟨ idR ⟩ |
| 351 f | |
| 352 ∎ | |
| 652 | 353 |
| 654 | 354 unique : {a : Obj B} { b : Obj A } → { f : Hom B a (FObj U b) } → { g : Hom A (obj (i a)) b} → |
| 355 B [ B [ FMap U g o tmap-η a ] ≈ f ] → A [ arrow (solution f) ≈ g ] | |
| 356 unique {a} {b} {f} {g} ugη=f = let open ≈-Reasoning A in begin | |
| 357 arrow (solution f) | |
| 1106 | 358 ≈↑⟨ ≈←≡ ( cong (λ k → arrow (solution k)) ( (≡←≈ B) ugη=f )) ⟩ |
| 654 | 359 arrow (solution (B [ FMap U g o tmap-η a ] )) |
| 360 ≈↑⟨ uniqueness (In a) (record { arrow = g ; comm = comm1 }) ⟩ | |
| 361 g | |
| 362 ∎ where | |
|
691
917e51be9bbf
change argument of Limit and K
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
690
diff
changeset
|
363 comm1 : B [ B [ FMap U g o hom (i a) ] ≈ B [ B [ FMap U g o tmap-η a ] o FMap (K A B a) g ] ] |
| 654 | 364 comm1 = let open ≈-Reasoning B in sym idR |
| 645 | 365 |
|
690
3d41a8edbf63
fix universal mapping done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
689
diff
changeset
|
366 UM : UniversalMapping B A U |
| 655 | 367 UM = record { |
|
690
3d41a8edbf63
fix universal mapping done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
689
diff
changeset
|
368 F = λ b → obj (i b) ; |
|
3d41a8edbf63
fix universal mapping done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
689
diff
changeset
|
369 η = tmap-η ; |
| 655 | 370 _* = λ f → arrow (solution f) ; |
| 371 isUniversalMapping = record { | |
| 372 universalMapping = λ {a} {b} {f} → univ f ; | |
| 373 uniquness = unique | |
| 374 }} | |
| 375 | |
| 659 | 376 -- Adjoint can be built as follows (same as univeral-mapping.agda ) |
| 377 -- | |
| 378 -- F : Functor B A | |
| 379 -- F = record { | |
| 380 -- FObj = λ b → obj (i b) | |
| 381 -- ; FMap = λ {x} {y} (f : Hom B x y ) → arrow (solution ( B [ tmap-η y o f ] )) | |
| 645 | 382 |
| 659 | 383 -- nat-ε : NTrans A A (F ○ U) identityFunctor |
| 384 -- nat-ε = record { | |
| 385 -- TMap = λ x → arrow ( solution (id1 B (FObj U x))) | |
| 645 | 386 |
| 659 | 387 -- nat-η : NTrans B B identityFunctor (U ○ F) |
| 388 -- nat-η = record { TMap = λ y → tmap-η y ; isNTrans = record { commute = comm1 } } where | |
| 645 | 389 |
| 659 | 390 -- FisLeftAdjoint : Adjunction B A U F nat-η nat-ε |
| 391 -- FisLeftAdjoint = record { isAdjunction = record { | |
| 392 | |
| 1107 | 393 open import Data.Product renaming (_×_ to _∧_ ) hiding ( <_,_> ) |
| 394 open import Category.Constructions.Product | |
| 395 | |
| 396 module pro-ex {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) ( _*_ : Obj A → Obj A → Obj A ) | |
| 397 (*-iso : (a b c x : Obj A) → IsoS A (A × A) x c (x , x ) (a , b )) where | |
| 398 | |
| 399 -- Hom A x c ≅ ( Hom A x a ) * ( Hom A x b ) | |
| 400 | |
| 401 open IsoS | |
| 402 | |
| 1111 | 403 -- import Axiom.Extensionality.Propositional |
| 404 -- postulate f-extensionality : { n m : Level} → Axiom.Extensionality.Propositional.Extensionality n m | |
| 1107 | 405 |
| 406 open import Category.Cat | |
| 407 | |
| 408 *eq : {a b : Obj (A × A) } { x y : Hom (A × A) a b } → (x≈y : (A × A) [ x ≈ y ]) → x ≡ y | |
| 409 *eq {a} {b} {x1 , x2} {y1 , y2} (eq1 , eq2) = cong₂ _,_ ( ≡←≈ A eq1 ) ( ≡←≈ A eq2 ) | |
| 410 | |
| 411 opA = Category.op A | |
| 412 prodFunctor : Functor (Category.op A) (Category.op (A × A)) | |
| 413 prodFunctor = record { | |
| 414 FObj = λ x → x , x | |
| 415 ; FMap = λ {x} {y} (f : Hom opA x y ) → f , f | |
| 1111 | 416 ; isFunctor = record { identity = refl-hom , refl-hom ; distr = refl-hom , refl-hom ; ≈-cong = λ eq → eq , eq } |
| 417 } where open ≈-Reasoning A | |
| 1107 | 418 t00 : (a c d e : Obj opA) (f : Hom opA a c ) → Hom (A × A) (c , c) (d , e ) |
| 419 t00 a c d e f = ≅→ (*-iso d e a c) f | |
| 1112 | 420 -- nat-* : {a b c : Obj A} → NTrans (Category.op A) (Sets {c₂}) (Yoneda A (≡←≈ A) c ) (Yoneda (A × A) *eq (a , b) ○ prodFunctor ) |
| 421 -- nat-* {a} {b} {c} = record { TMap = λ z f → ≅→ (*-iso a b c z) f ; isNTrans = record { commute = nat-comm } } where | |
| 422 -- nat-comm : {x y : Obj opA} {f : Hom opA x y} → | |
| 423 -- Sets [ Sets [ (λ g → opA [ f o proj₁ g ] , opA [ f o proj₂ g ]) o (λ f₁ → ≅→ (*-iso a b c x) f₁) ] | |
| 424 -- ≈ Sets [ (λ f₁ → ≅→ (*-iso a b c y) f₁) o (λ g → opA [ f o g ]) ] ] | |
| 425 -- nat-comm {x} {y} {f} g = cong₂ _,_ ( ≡←≈ A ( begin | |
| 426 -- proj₁ (≅→ (*-iso a b c x) g) o f ≈⟨ ? ⟩ | |
| 427 -- proj₁ (≅→ (*-iso a b c y) (A [ g o f ])) ∎ )) ( ≡←≈ A ( begin | |
| 428 -- ? ≈⟨ ? ⟩ | |
| 429 -- ? ∎ )) where | |
| 430 -- open ≈-Reasoning A | |
| 431 -- | |
| 1107 | 432 |
| 433 | |
| 659 | 434 -- end |
| 435 |