Mercurial > hg > Members > kono > Proof > category
annotate freyd2.agda @ 629:693020c766d2
fix
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Mon, 26 Jun 2017 17:41:02 +0900 |
parents | b99660fa14e1 |
children | d2fc6fb58e0e |
rev | line source |
---|---|
497
e8b85a05a6b2
add if U is iso to representable functor then preserve limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
1 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
|
2 open import Level |
611
b1b5c6b4c570
natural transformation in representable functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
610
diff
changeset
|
3 open import Category.Sets renaming ( _o_ to _*_ ) |
497
e8b85a05a6b2
add if U is iso to representable functor then preserve limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
4 |
e8b85a05a6b2
add if U is iso to representable functor then preserve limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
5 module freyd2 |
e8b85a05a6b2
add if U is iso to representable functor then preserve limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
6 where |
e8b85a05a6b2
add if U is iso to representable functor then preserve limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
7 |
e8b85a05a6b2
add if U is iso to representable functor then preserve limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
8 open import HomReasoning |
e8b85a05a6b2
add if U is iso to representable functor then preserve limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
9 open import cat-utility |
e8b85a05a6b2
add if U is iso to representable functor then preserve limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
10 open import Relation.Binary.Core |
e8b85a05a6b2
add if U is iso to representable functor then preserve limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
11 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
|
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 ---------- |
e8b85a05a6b2
add if U is iso to representable functor then preserve limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
14 -- |
e8b85a05a6b2
add if U is iso to representable functor then preserve limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
15 -- 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
|
16 -- 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
|
17 -- 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
|
18 -- |
e8b85a05a6b2
add if U is iso to representable functor then preserve limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
19 |
617
34540494fdcf
initital obj uniquness done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
616
diff
changeset
|
20 -- maybe this is a part of local smallness |
611
b1b5c6b4c570
natural transformation in representable functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
610
diff
changeset
|
21 postulate ≈-≡ : { 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
|
22 |
e8b85a05a6b2
add if U is iso to representable functor then preserve limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
23 import Relation.Binary.PropositionalEquality |
e8b85a05a6b2
add if U is iso to representable functor then preserve limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
24 -- 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 ) |
e8b85a05a6b2
add if U is iso to representable functor then preserve limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
25 postulate extensionality : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) → Relation.Binary.PropositionalEquality.Extensionality c₂ c₂ |
e8b85a05a6b2
add if U is iso to representable functor then preserve limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
26 |
624
9b9bc1e076f3
introduce one element set
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
623
diff
changeset
|
27 |
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 ---- |
e8b85a05a6b2
add if U is iso to representable functor then preserve limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
29 -- |
617
34540494fdcf
initital obj uniquness done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
616
diff
changeset
|
30 -- 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
|
31 -- |
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 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
|
35 open Functor |
498
c981a2f0642f
UpreseveLimit detailing
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
497
diff
changeset
|
36 open Limit |
c981a2f0642f
UpreseveLimit detailing
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
497
diff
changeset
|
37 open IsLimit |
c981a2f0642f
UpreseveLimit detailing
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
497
diff
changeset
|
38 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
|
39 |
616 | 40 Yoneda : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) (a : Obj A) → Functor A (Sets {c₂}) |
41 Yoneda {c₁} {c₂} {ℓ} A a = record { | |
497
e8b85a05a6b2
add if U is iso to representable functor then preserve limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
42 FObj = λ b → Hom A a b |
e8b85a05a6b2
add if U is iso to representable functor then preserve limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
43 ; FMap = λ {x} {y} (f : Hom A x y ) → λ ( g : Hom A a x ) → A [ f o g ] -- f : Hom A x y → Hom Sets (Hom A a x ) (Hom A a y) |
e8b85a05a6b2
add if U is iso to representable functor then preserve limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
44 ; isFunctor = record { |
e8b85a05a6b2
add if U is iso to representable functor then preserve limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
45 identity = λ {b} → extensionality A ( λ x → lemma-y-obj1 {b} x ) ; |
e8b85a05a6b2
add if U is iso to representable functor then preserve limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
46 distr = λ {a} {b} {c} {f} {g} → extensionality A ( λ x → lemma-y-obj2 a b c f g x ) ; |
e8b85a05a6b2
add if U is iso to representable functor then preserve limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
47 ≈-cong = λ eq → extensionality A ( λ x → lemma-y-obj3 x eq ) |
e8b85a05a6b2
add if U is iso to representable functor then preserve limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
48 } |
e8b85a05a6b2
add if U is iso to representable functor then preserve limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
49 } where |
e8b85a05a6b2
add if U is iso to representable functor then preserve limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
50 lemma-y-obj1 : {b : Obj A } → (x : Hom A a b) → A [ id1 A b o x ] ≡ x |
611
b1b5c6b4c570
natural transformation in representable functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
610
diff
changeset
|
51 lemma-y-obj1 {b} x = let open ≈-Reasoning A in ≈-≡ A idL |
497
e8b85a05a6b2
add if U is iso to representable functor then preserve limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
52 lemma-y-obj2 : (a₁ b c : Obj A) (f : Hom A a₁ b) (g : Hom A b c ) → (x : Hom A a a₁ )→ |
e8b85a05a6b2
add if U is iso to representable functor then preserve limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
53 A [ A [ g o f ] o x ] ≡ (Sets [ _[_o_] A g o _[_o_] A f ]) x |
611
b1b5c6b4c570
natural transformation in representable functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
610
diff
changeset
|
54 lemma-y-obj2 a₁ b c f g x = let open ≈-Reasoning A in ≈-≡ A ( begin |
497
e8b85a05a6b2
add if U is iso to representable functor then preserve limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
55 A [ A [ g o f ] o x ] |
e8b85a05a6b2
add if U is iso to representable functor then preserve limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
56 ≈↑⟨ assoc ⟩ |
e8b85a05a6b2
add if U is iso to representable functor then preserve limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
57 A [ g o A [ f o x ] ] |
e8b85a05a6b2
add if U is iso to representable functor then preserve limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
58 ≈⟨⟩ |
e8b85a05a6b2
add if U is iso to representable functor then preserve limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
59 ( λ x → A [ g o x ] ) ( ( λ x → A [ f o x ] ) x ) |
e8b85a05a6b2
add if U is iso to representable functor then preserve limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
60 ∎ ) |
e8b85a05a6b2
add if U is iso to representable functor then preserve limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
61 lemma-y-obj3 : {b c : Obj A} {f g : Hom A b c } → (x : Hom A a b ) → A [ f ≈ g ] → A [ f o x ] ≡ A [ g o x ] |
611
b1b5c6b4c570
natural transformation in representable functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
610
diff
changeset
|
62 lemma-y-obj3 {_} {_} {f} {g} x eq = let open ≈-Reasoning A in ≈-≡ A ( begin |
497
e8b85a05a6b2
add if U is iso to representable functor then preserve limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
63 A [ f o x ] |
e8b85a05a6b2
add if U is iso to representable functor then preserve limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
64 ≈⟨ resp refl-hom eq ⟩ |
e8b85a05a6b2
add if U is iso to representable functor then preserve limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
65 A [ g o x ] |
e8b85a05a6b2
add if U is iso to representable functor then preserve limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
66 ∎ ) |
e8b85a05a6b2
add if U is iso to representable functor then preserve limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
67 |
609 | 68 -- Representable U ≈ Hom(A,-) |
502 | 69 |
609 | 70 record Representable { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) ( U : Functor A (Sets {c₂}) ) (a : Obj A) : Set (suc ℓ ⊔ (suc (suc c₂) ⊔ suc c₁ )) where |
502 | 71 field |
72 -- FObj U x : A → Set | |
609 | 73 -- FMap U f = Set → Set (locally small) |
502 | 74 -- λ b → Hom (a,b) : A → Set |
75 -- λ f → Hom (a,-) = λ b → Hom a b | |
76 | |
616 | 77 repr→ : NTrans A (Sets {c₂}) U (Yoneda A a ) |
78 repr← : NTrans A (Sets {c₂}) (Yoneda A a) U | |
79 reprId→ : {x : Obj A} → Sets [ Sets [ TMap repr→ x o TMap repr← x ] ≈ id1 (Sets {c₂}) (FObj (Yoneda A a) x )] | |
609 | 80 reprId← : {x : Obj A} → Sets [ Sets [ TMap repr← x o TMap repr→ x ] ≈ id1 (Sets {c₂}) (FObj U x)] |
608 | 81 |
609 | 82 open Representable |
608 | 83 open import freyd |
502 | 84 |
624
9b9bc1e076f3
introduce one element set
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
623
diff
changeset
|
85 _↓_ : { 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
|
86 → ( F G : Functor A B ) |
9b9bc1e076f3
introduce one element set
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
623
diff
changeset
|
87 → Category (c₂' ⊔ c₁) (ℓ' ⊔ c₂) ℓ |
9b9bc1e076f3
introduce one element set
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
623
diff
changeset
|
88 _↓_ { 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
|
89 where open import Comma1 F G |
9b9bc1e076f3
introduce one element set
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
623
diff
changeset
|
90 |
9b9bc1e076f3
introduce one element set
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
623
diff
changeset
|
91 open import freyd |
9b9bc1e076f3
introduce one element set
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
623
diff
changeset
|
92 open SmallFullSubcategory |
9b9bc1e076f3
introduce one element set
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
623
diff
changeset
|
93 open Complete |
9b9bc1e076f3
introduce one element set
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
623
diff
changeset
|
94 open PreInitial |
9b9bc1e076f3
introduce one element set
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
623
diff
changeset
|
95 open HasInitialObject |
9b9bc1e076f3
introduce one element set
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
623
diff
changeset
|
96 open import Comma1 |
9b9bc1e076f3
introduce one element set
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
623
diff
changeset
|
97 open CommaObj |
609 | 98 open LimitPreserve |
608 | 99 |
609 | 100 -- Representable Functor U preserve limit , so K{*}↓U is complete |
610 | 101 -- |
616 | 102 -- 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
|
103 -- : Functor Sets A |
610 | 104 |
105 UpreserveLimit0 : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (I : Category c₁ c₂ ℓ) | |
612 | 106 (b : Obj A ) |
610 | 107 (Γ : Functor I A) (limita : Limit A I Γ) → |
616 | 108 IsLimit Sets I (Yoneda A b ○ Γ) (FObj (Yoneda A b) (a0 limita)) (LimitNat A I Sets Γ (a0 limita) (t0 limita) (Yoneda A b)) |
612 | 109 UpreserveLimit0 {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
|
110 limit = λ a t → ψ a t |
b1b5c6b4c570
natural transformation in representable functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
610
diff
changeset
|
111 ; 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
|
112 ; limit-uniqueness = λ {b} {t} {f} t0f=t → limit-uniqueness0 {b} {t} {f} t0f=t |
610 | 113 } where |
616 | 114 hat0 : NTrans I Sets (K Sets I (FObj (Yoneda A b) (a0 lim))) (Yoneda A b ○ Γ) |
115 hat0 = LimitNat A I Sets Γ (a0 lim) (t0 lim) (Yoneda A b) | |
611
b1b5c6b4c570
natural transformation in representable functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
610
diff
changeset
|
116 haa0 : Obj Sets |
616 | 117 haa0 = FObj (Yoneda A b) (a0 lim) |
118 ta : (a : Obj Sets) ( x : a ) ( t : NTrans I Sets (K Sets I a) (Yoneda A b ○ Γ)) → NTrans I A (K A I b ) Γ | |
611
b1b5c6b4c570
natural transformation in representable functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
610
diff
changeset
|
119 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
|
120 commute1 : {a₁ b₁ : Obj I} {f : Hom I a₁ b₁} → |
b1b5c6b4c570
natural transformation in representable functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
610
diff
changeset
|
121 A [ A [ FMap Γ f o TMap t a₁ x ] ≈ A [ TMap t b₁ x o FMap (K A I b) f ] ] |
b1b5c6b4c570
natural transformation in representable functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
610
diff
changeset
|
122 commute1 {a₁} {b₁} {f} = let open ≈-Reasoning A in begin |
b1b5c6b4c570
natural transformation in representable functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
610
diff
changeset
|
123 FMap Γ f o TMap t a₁ x |
b1b5c6b4c570
natural transformation in representable functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
610
diff
changeset
|
124 ≈⟨⟩ |
616 | 125 ( ( FMap (Yoneda A b ○ Γ ) f ) * TMap t a₁ ) x |
611
b1b5c6b4c570
natural transformation in representable functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
610
diff
changeset
|
126 ≈⟨ ≡-≈ ( cong (λ k → k x ) (IsNTrans.commute (isNTrans t)) ) ⟩ |
b1b5c6b4c570
natural transformation in representable functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
610
diff
changeset
|
127 ( TMap t b₁ * ( FMap (K Sets I a) f ) ) x |
b1b5c6b4c570
natural transformation in representable functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
610
diff
changeset
|
128 ≈⟨⟩ |
b1b5c6b4c570
natural transformation in representable functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
610
diff
changeset
|
129 ( TMap t b₁ * id1 Sets a ) x |
b1b5c6b4c570
natural transformation in representable functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
610
diff
changeset
|
130 ≈⟨⟩ |
b1b5c6b4c570
natural transformation in representable functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
610
diff
changeset
|
131 TMap t b₁ x |
b1b5c6b4c570
natural transformation in representable functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
610
diff
changeset
|
132 ≈↑⟨ idR ⟩ |
b1b5c6b4c570
natural transformation in representable functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
610
diff
changeset
|
133 TMap t b₁ x o id1 A b |
b1b5c6b4c570
natural transformation in representable functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
610
diff
changeset
|
134 ≈⟨⟩ |
b1b5c6b4c570
natural transformation in representable functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
610
diff
changeset
|
135 TMap t b₁ x o FMap (K A I b) f |
b1b5c6b4c570
natural transformation in representable functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
610
diff
changeset
|
136 ∎ |
616 | 137 ψ : (X : Obj Sets) ( t : NTrans I Sets (K Sets I X) (Yoneda A b ○ Γ)) |
138 → Hom Sets X (FObj (Yoneda A b) (a0 lim)) | |
139 ψ X t x = FMap (Yoneda A b) (limit (isLimit lim) b (ta X x t )) (id1 A b ) | |
140 t0f=t0 : (a : Obj Sets ) ( t : NTrans I Sets (K Sets I a) (Yoneda A b ○ Γ)) (i : Obj I) | |
141 → Sets [ Sets [ TMap (LimitNat A I Sets Γ (a0 lim) (t0 lim) (Yoneda A b)) i o ψ a t ] ≈ TMap t i ] | |
612 | 142 t0f=t0 a t i = let open ≈-Reasoning A in extensionality A ( λ x → ≈-≡ A ( begin |
616 | 143 ( Sets [ TMap (LimitNat A I Sets Γ (a0 lim) (t0 lim) (Yoneda A b)) i o ψ a t ] ) x |
612 | 144 ≈⟨⟩ |
616 | 145 FMap (Yoneda A b) ( TMap (t0 lim) i) (FMap (Yoneda 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
|
146 ≈⟨⟩ -- FMap (Hom A b ) f g = A [ f o g ] |
613 | 147 TMap (t0 lim) i o (limit (isLimit lim) b (ta a x t ) o id1 A b ) |
148 ≈⟨ cdr idR ⟩ | |
149 TMap (t0 lim) i o limit (isLimit lim) b (ta a x t ) | |
150 ≈⟨ t0f=t (isLimit lim) ⟩ | |
151 TMap (ta a x t) i | |
152 ≈⟨⟩ | |
612 | 153 TMap t i x |
154 ∎ )) | |
616 | 155 limit-uniqueness0 : {a : Obj Sets} {t : NTrans I Sets (K Sets I a) (Yoneda A b ○ Γ)} {f : Hom Sets a (FObj (Yoneda A b) (a0 lim))} → |
156 ({i : Obj I} → Sets [ Sets [ TMap (LimitNat A I Sets Γ (a0 lim) (t0 lim) (Yoneda 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
|
157 Sets [ ψ a t ≈ f ] |
e6be03d94284
Representational Functor preserve limit done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
613
diff
changeset
|
158 limit-uniqueness0 {a} {t} {f} t0f=t = let open ≈-Reasoning A in extensionality A ( λ x → ≈-≡ A ( begin |
e6be03d94284
Representational Functor preserve limit done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
613
diff
changeset
|
159 ψ a t x |
e6be03d94284
Representational Functor preserve limit done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
613
diff
changeset
|
160 ≈⟨⟩ |
616 | 161 FMap (Yoneda 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
|
162 ≈⟨⟩ |
e6be03d94284
Representational Functor preserve limit done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
613
diff
changeset
|
163 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
|
164 ≈⟨ idR ⟩ |
e6be03d94284
Representational Functor preserve limit done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
613
diff
changeset
|
165 limit (isLimit lim) b (ta a x t ) |
e6be03d94284
Representational Functor preserve limit done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
613
diff
changeset
|
166 ≈⟨ limit-uniqueness (isLimit lim) ( λ {i} → ≡-≈ ( cong ( λ g → g x )( t0f=t {i} ))) ⟩ |
e6be03d94284
Representational Functor preserve limit done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
613
diff
changeset
|
167 f x |
e6be03d94284
Representational Functor preserve limit done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
613
diff
changeset
|
168 ∎ )) |
610 | 169 |
609 | 170 |
171 UpreserveLimit : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (I : Category c₁ c₂ ℓ) | |
616 | 172 (b : Obj A ) → LimitPreserve A I Sets (Yoneda A b) |
612 | 173 UpreserveLimit A I b = record { |
174 preserve = λ Γ lim → UpreserveLimit0 A I b Γ lim | |
610 | 175 } |
609 | 176 |
624
9b9bc1e076f3
introduce one element set
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
623
diff
changeset
|
177 |
608 | 178 -- K{*}↓U has preinitial full subcategory if U is representable |
609 | 179 -- if U is representable, K{*}↓U has initial Object ( so it has preinitial full subcategory ) |
608 | 180 |
617
34540494fdcf
initital obj uniquness done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
616
diff
changeset
|
181 open CommaHom |
34540494fdcf
initital obj uniquness done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
616
diff
changeset
|
182 |
627 | 183 data * {c : Level} : Set c where |
184 OneObj : * | |
185 | |
609 | 186 KUhasInitialObj : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) |
608 | 187 (a : Obj A ) |
628 | 188 → HasInitialObject ( K (Sets) A * ↓ (Yoneda A a) ) ( record { obj = a ; hom = λ x → id1 A a } ) |
621 | 189 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
|
190 initial = λ b → initial0 b |
624
9b9bc1e076f3
introduce one element set
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
623
diff
changeset
|
191 ; uniqueness = λ b f → unique b f |
615
a45c32ceca97
initial Object's arrow found
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
614
diff
changeset
|
192 } where |
621 | 193 commaCat : Category (c₂ ⊔ c₁) c₂ ℓ |
624
9b9bc1e076f3
introduce one element set
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
623
diff
changeset
|
194 commaCat = K Sets A * ↓ Yoneda A a |
9b9bc1e076f3
introduce one element set
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
623
diff
changeset
|
195 initObj : Obj (K Sets A * ↓ Yoneda A a) |
9b9bc1e076f3
introduce one element set
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
623
diff
changeset
|
196 initObj = record { obj = a ; hom = λ x → id1 A a } |
9b9bc1e076f3
introduce one element set
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
623
diff
changeset
|
197 comm2 : (b : Obj commaCat) ( x : * ) → ( Sets [ FMap (Yoneda A a) (hom b OneObj) o (λ x₁ → id1 A a) ] ) x ≡ hom b x |
9b9bc1e076f3
introduce one element set
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
623
diff
changeset
|
198 comm2 b OneObj = let open ≈-Reasoning A in ≈-≡ A ( begin |
9b9bc1e076f3
introduce one element set
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
623
diff
changeset
|
199 ( Sets [ FMap (Yoneda A a) (hom b OneObj) o (λ x₁ → id1 A a) ] ) OneObj |
9b9bc1e076f3
introduce one element set
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
623
diff
changeset
|
200 ≈⟨⟩ |
9b9bc1e076f3
introduce one element set
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
623
diff
changeset
|
201 FMap (Yoneda A a) (hom b OneObj) (id1 A a) |
9b9bc1e076f3
introduce one element set
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
623
diff
changeset
|
202 ≈⟨⟩ |
9b9bc1e076f3
introduce one element set
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
623
diff
changeset
|
203 hom b OneObj o id1 A a |
9b9bc1e076f3
introduce one element set
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
623
diff
changeset
|
204 ≈⟨ idR ⟩ |
9b9bc1e076f3
introduce one element set
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
623
diff
changeset
|
205 hom b OneObj |
9b9bc1e076f3
introduce one element set
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
623
diff
changeset
|
206 ∎ ) |
9b9bc1e076f3
introduce one element set
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
623
diff
changeset
|
207 comm1 : (b : Obj commaCat) → Sets [ Sets [ FMap (Yoneda A a) (hom b OneObj) o hom initObj ] ≈ Sets [ hom b o FMap (K Sets A *) (hom b OneObj) ] ] |
9b9bc1e076f3
introduce one element set
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
623
diff
changeset
|
208 comm1 b = let open ≈-Reasoning Sets in begin |
9b9bc1e076f3
introduce one element set
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
623
diff
changeset
|
209 FMap (Yoneda A a) (hom b OneObj) o ( λ x → id1 A a ) |
9b9bc1e076f3
introduce one element set
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
623
diff
changeset
|
210 ≈⟨ extensionality A ( λ x → comm2 b x ) ⟩ |
9b9bc1e076f3
introduce one element set
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
623
diff
changeset
|
211 hom b |
615
a45c32ceca97
initial Object's arrow found
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
614
diff
changeset
|
212 ≈⟨⟩ |
624
9b9bc1e076f3
introduce one element set
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
623
diff
changeset
|
213 hom b o FMap (K Sets A *) (hom b OneObj) |
615
a45c32ceca97
initial Object's arrow found
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
614
diff
changeset
|
214 ∎ |
624
9b9bc1e076f3
introduce one element set
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
623
diff
changeset
|
215 initial0 : (b : Obj commaCat) → |
9b9bc1e076f3
introduce one element set
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
623
diff
changeset
|
216 Hom commaCat initObj b |
615
a45c32ceca97
initial Object's arrow found
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
614
diff
changeset
|
217 initial0 b = record { |
624
9b9bc1e076f3
introduce one element set
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
623
diff
changeset
|
218 arrow = hom b OneObj |
9b9bc1e076f3
introduce one element set
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
623
diff
changeset
|
219 ; comm = comm1 b } |
625 | 220 -- what is comm f ? |
221 comm-f : (b : Obj (K Sets A * ↓ (Yoneda A a))) (f : Hom (K Sets A * ↓ Yoneda A a) initObj b) | |
222 → Sets [ Sets [ FMap (Yoneda A a) (arrow f) o ( λ x → id1 A a ) ] | |
223 ≈ Sets [ hom b o FMap (K Sets A *) (arrow f) ] ] | |
224 comm-f b f = comm f | |
624
9b9bc1e076f3
introduce one element set
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
623
diff
changeset
|
225 unique : (b : Obj (K Sets A * ↓ Yoneda A a)) (f : Hom (K Sets A * ↓ Yoneda A a) initObj b) |
9b9bc1e076f3
introduce one element set
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
623
diff
changeset
|
226 → (K Sets A * ↓ Yoneda A a) [ f ≈ initial0 b ] |
9b9bc1e076f3
introduce one element set
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
623
diff
changeset
|
227 unique b f = let open ≈-Reasoning A in begin |
9b9bc1e076f3
introduce one element set
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
623
diff
changeset
|
228 arrow f |
9b9bc1e076f3
introduce one element set
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
623
diff
changeset
|
229 ≈↑⟨ idR ⟩ |
9b9bc1e076f3
introduce one element set
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
623
diff
changeset
|
230 arrow f o id1 A a |
9b9bc1e076f3
introduce one element set
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
623
diff
changeset
|
231 ≈⟨⟩ |
9b9bc1e076f3
introduce one element set
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
623
diff
changeset
|
232 ( Sets [ FMap (Yoneda A a) (arrow f) o id1 Sets (FObj (Yoneda A a) a) ] ) (id1 A a) |
625 | 233 ≈⟨⟩ |
234 ( Sets [ FMap (Yoneda A a) (arrow f) o ( λ x → id1 A a ) ] ) OneObj | |
235 ≈⟨ ≡-≈ ( cong (λ k → k OneObj ) (comm f )) ⟩ | |
624
9b9bc1e076f3
introduce one element set
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
623
diff
changeset
|
236 ( Sets [ hom b o FMap (K Sets A *) (arrow f) ] ) OneObj |
9b9bc1e076f3
introduce one element set
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
623
diff
changeset
|
237 ≈⟨⟩ |
9b9bc1e076f3
introduce one element set
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
623
diff
changeset
|
238 hom b OneObj |
9b9bc1e076f3
introduce one element set
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
623
diff
changeset
|
239 ∎ |
9b9bc1e076f3
introduce one element set
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
623
diff
changeset
|
240 |
615
a45c32ceca97
initial Object's arrow found
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
614
diff
changeset
|
241 |
a45c32ceca97
initial Object's arrow found
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
614
diff
changeset
|
242 |
a45c32ceca97
initial Object's arrow found
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
614
diff
changeset
|
243 -- K{*}↓U has preinitial full subcategory then U is representable |
a45c32ceca97
initial Object's arrow found
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
614
diff
changeset
|
244 |
617
34540494fdcf
initital obj uniquness done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
616
diff
changeset
|
245 open SmallFullSubcategory |
34540494fdcf
initital obj uniquness done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
616
diff
changeset
|
246 open PreInitial |
626 | 247 |
248 ≡-cong = Relation.Binary.PropositionalEquality.cong | |
249 | |
628 | 250 |
627 | 251 UisRepresentable : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) |
626 | 252 (U : Functor A (Sets {c₂}) ) |
628 | 253 (SFS : SmallFullSubcategory ( K (Sets {c₂}) A * ↓ U) ) |
629 | 254 (PI : PreInitial ( K (Sets) A * ↓ U) (SFSF SFS)) |
626 | 255 → Representable A U (obj (preinitialObj PI )) |
629 | 256 UisRepresentable A U SFS PI = record { |
627 | 257 repr→ = record { TMap = tmap1 ; isNTrans = record { commute = comm1 } } |
626 | 258 ; repr← = record { TMap = tmap2 ; isNTrans = record { commute = comm2 } } |
628 | 259 ; reprId→ = {!!} |
260 ; reprId← = {!!} | |
626 | 261 } where |
629 | 262 pi : Obj ( K (Sets) A * ↓ U) |
263 pi = preinitialObj PI | |
264 ub : (b : Obj A) (x : FObj U b ) → Hom Sets (FObj (K Sets A *) b) (FObj U b) | |
265 ub b x OneObj = x | |
628 | 266 tmap1 : (b : Obj A) → Hom Sets (FObj U b) (FObj (Yoneda A (obj pi)) b) |
629 | 267 tmap1 b x = arrow ( SFSFMap← SFS ( preinitialArrow PI {FObj (SFSF SFS) (record { obj = b ; hom = ub b x}) } )) |
626 | 268 tmap2 : (b : Obj A) → Hom Sets (FObj (Yoneda A (obj (preinitialObj PI))) b) (FObj U b) |
269 tmap2 b x = ( FMap U x ) ( hom ( preinitialObj PI ) OneObj ) | |
629 | 270 comm11 : (a b : Obj A) (f : Hom A a b) (y : FObj U a ) → |
271 ( Sets [ FMap (Yoneda A (obj (preinitialObj PI))) f o | |
272 ( λ x → arrow ( SFSFMap← SFS ( preinitialArrow PI {FObj (SFSF SFS) (record { obj = a ; hom = ub a x}) } ))) ] ) y | |
273 ≡ (Sets [ ( λ x → arrow ( SFSFMap← SFS ( preinitialArrow PI {FObj (SFSF SFS) (record { obj = b ; hom = ub b x}) } ))) o FMap U f ] ) y | |
274 comm11 a b f y = begin | |
275 ( Sets [ FMap (Yoneda A (obj (preinitialObj PI))) f o | |
276 ( λ x → arrow ( SFSFMap← SFS ( preinitialArrow PI {FObj (SFSF SFS) (record { obj = a ; hom = ub a x}) } ))) ] ) y | |
277 ≡⟨⟩ | |
278 A [ f o arrow ( SFSFMap← SFS ( preinitialArrow PI {FObj (SFSF SFS) (record { obj = a ; hom = ub a y}) } )) ] | |
279 ≡⟨ {!!} ⟩ | |
280 arrow ( SFSFMap← SFS ( preinitialArrow PI {FObj (SFSF SFS) (record { obj = b ; hom = ub b (FMap U f y) } ) } ) ) | |
281 ≡⟨⟩ | |
282 (Sets [ ( λ x → arrow ( SFSFMap← SFS ( preinitialArrow PI {FObj (SFSF SFS) (record { obj = b ; hom = ub b x}) } ))) o FMap U f ] ) y | |
283 ∎ where | |
284 open import Relation.Binary.PropositionalEquality | |
285 open ≡-Reasoning | |
626 | 286 comm1 : {a b : Obj A} {f : Hom A a b} → Sets [ Sets [ FMap (Yoneda A (obj (preinitialObj PI))) f o tmap1 a ] ≈ Sets [ tmap1 b o FMap U f ] ] |
287 comm1 {a} {b} {f} = let open ≈-Reasoning Sets in begin | |
288 FMap (Yoneda A (obj (preinitialObj PI))) f o tmap1 a | |
629 | 289 ≈⟨⟩ |
290 FMap (Yoneda A (obj (preinitialObj PI))) f o ( λ x → arrow ( SFSFMap← SFS ( preinitialArrow PI {FObj (SFSF SFS) (record { obj = a ; hom = ub a x}) } ))) | |
291 ≈⟨ extensionality Sets ( λ y → comm11 a b f y ) ⟩ | |
292 ( λ x → arrow ( SFSFMap← SFS ( preinitialArrow PI {FObj (SFSF SFS) (record { obj = b ; hom = ub b x}) } ))) o FMap U f | |
293 ≈⟨⟩ | |
626 | 294 tmap1 b o FMap U f |
295 ∎ | |
296 comm21 : (a b : Obj A) (f : Hom A a b) ( y : Hom A (obj (preinitialObj PI)) a ) → | |
297 (Sets [ FMap U f o (λ x → FMap U x (hom (preinitialObj PI) OneObj))] ) y ≡ | |
298 (Sets [ ( λ x → (FMap U x ) (hom (preinitialObj PI) OneObj)) o (λ x → A [ f o x ] ) ] ) y | |
299 comm21 a b f y = begin | |
300 FMap U f ( FMap U y (hom (preinitialObj PI) OneObj)) | |
301 ≡⟨ ≡-cong ( λ k → k (hom (preinitialObj PI) OneObj)) ( sym ( IsFunctor.distr (isFunctor U ) ) ) ⟩ | |
302 (FMap U (A [ f o y ] ) ) (hom (preinitialObj PI) OneObj) | |
303 ∎ where | |
304 open import Relation.Binary.PropositionalEquality | |
305 open ≡-Reasoning | |
306 comm2 : {a b : Obj A} {f : Hom A a b} → Sets [ Sets [ FMap U f o tmap2 a ] ≈ | |
307 Sets [ tmap2 b o FMap (Yoneda A (obj (preinitialObj PI))) f ] ] | |
308 comm2 {a} {b} {f} = let open ≈-Reasoning Sets in begin | |
309 FMap U f o tmap2 a | |
310 ≈⟨⟩ | |
311 FMap U f o ( λ x → ( FMap U x ) ( hom ( preinitialObj PI ) OneObj ) ) | |
312 ≈⟨ extensionality Sets ( λ y → comm21 a b f y ) ⟩ | |
313 ( λ x → ( FMap U x ) ( hom ( preinitialObj PI ) OneObj ) ) o ( λ x → A [ f o x ] ) | |
314 ≈⟨⟩ | |
315 ( λ x → ( FMap U x ) ( hom ( preinitialObj PI ) OneObj ) ) o FMap (Yoneda A (obj (preinitialObj PI))) f | |
316 ≈⟨⟩ | |
317 tmap2 b o FMap (Yoneda A (obj (preinitialObj PI))) f | |
318 ∎ |