Mercurial > hg > Members > kono > Proof > category

annotate freyd2.agda @ 634:5b0286e3aa32

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fix
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Wed, 28 Jun 2017 17:17:17 +0900
parents 37fa9d3fab8c
children f7cc0ec00e05
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
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
7011165c118e on going ..
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 615
diff changeset
40 Yoneda : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) (a : Obj A) → Functor A (Sets {c₂})
7011165c118e on going ..
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 615
diff changeset
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
d686d7ae38e0 on goging
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 608
diff changeset
68 -- Representable U ≈　Hom(A,-)
502
01a0dda67a8b on going ..
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 499
diff changeset
69
609
d686d7ae38e0 on goging
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 608
diff changeset
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
01a0dda67a8b on going ..
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 499
diff changeset
71 field
01a0dda67a8b on going ..
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 499
diff changeset
72 -- FObj U x : A → Set
609
d686d7ae38e0 on goging
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 608
diff changeset
73 -- FMap U f = Set → Set (locally small)
502
01a0dda67a8b on going ..
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 499
diff changeset
74 -- λ b → Hom (a,b) : A → Set
01a0dda67a8b on going ..
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 499
diff changeset
75 -- λ f → Hom (a,-) = λ b → Hom a b
01a0dda67a8b on going ..
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 499
diff changeset
76
616
7011165c118e on going ..
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 615
diff changeset
77 repr→ : NTrans A (Sets {c₂}) U (Yoneda A a )
7011165c118e on going ..
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 615
diff changeset
78 repr← : NTrans A (Sets {c₂}) (Yoneda A a) U
7011165c118e on going ..
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 615
diff changeset
79 reprId→ : {x : Obj A} → Sets [ Sets [ TMap repr→ x o TMap repr← x ] ≈ id1 (Sets {c₂}) (FObj (Yoneda A a) x )]
609
d686d7ae38e0 on goging
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 608
diff changeset
80 reprId← : {x : Obj A} → Sets [ Sets [ TMap repr← x o TMap repr→ x ] ≈ id1 (Sets {c₂}) (FObj U x)]
608
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 502
diff changeset
81
609
d686d7ae38e0 on goging
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 608
diff changeset
82 open Representable
608
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 502
diff changeset
83 open import freyd
502
01a0dda67a8b on going ..
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 499
diff changeset
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
d686d7ae38e0 on goging
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 608
diff changeset
98 open LimitPreserve
608
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 502
diff changeset
99
609
d686d7ae38e0 on goging
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 608
diff changeset
100 -- Representable Functor U preserve limit , so K{*}↓U is complete
610
3fb4d834c349 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 609
diff changeset
101 --
616
7011165c118e on going ..
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 615
diff changeset
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
3fb4d834c349 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 609
diff changeset
104
3fb4d834c349 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 609
diff changeset
105 UpreserveLimit0 : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (I : Category c₁ c₂ ℓ)
612
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 611
diff changeset
106 (b : Obj A )
610
3fb4d834c349 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 609
diff changeset
107 (Γ : Functor I A) (limita : Limit A I Γ) →
616
7011165c118e on going ..
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 615
diff changeset
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
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 611
diff changeset
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
3fb4d834c349 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 609
diff changeset
113 } where
616
7011165c118e on going ..
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 615
diff changeset
114 hat0 : NTrans I Sets (K Sets I (FObj (Yoneda A b) (a0 lim))) (Yoneda A b ○ Γ)
7011165c118e on going ..
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 615
diff changeset
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
7011165c118e on going ..
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 615
diff changeset
117 haa0 = FObj (Yoneda A b) (a0 lim)
7011165c118e on going ..
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 615
diff changeset
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
7011165c118e on going ..
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 615
diff changeset
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
7011165c118e on going ..
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 615
diff changeset
137 ψ : (X : Obj Sets) ( t : NTrans I Sets (K Sets I X) (Yoneda A b ○ Γ))
7011165c118e on going ..
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 615
diff changeset
138 → Hom Sets X (FObj (Yoneda A b) (a0 lim))
7011165c118e on going ..
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 615
diff changeset
139 ψ X t x = FMap (Yoneda A b) (limit (isLimit lim) b (ta X x t )) (id1 A b )
7011165c118e on going ..
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 615
diff changeset
140 t0f=t0 : (a : Obj Sets ) ( t : NTrans I Sets (K Sets I a) (Yoneda A b ○ Γ)) (i : Obj I)
7011165c118e on going ..
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 615
diff changeset
141 → Sets [ Sets [ TMap (LimitNat A I Sets Γ (a0 lim) (t0 lim) (Yoneda A b)) i o ψ a t ] ≈ TMap t i ]
612
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 611
diff changeset
142 t0f=t0 a t i = let open ≈-Reasoning A in extensionality A ( λ x → ≈-≡ A ( begin
616
7011165c118e on going ..
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 615
diff changeset
143 ( Sets [ TMap (LimitNat A I Sets Γ (a0 lim) (t0 lim) (Yoneda A b)) i o ψ a t ] ) x
612
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 611
diff changeset
144 ≈⟨⟩
616
7011165c118e on going ..
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 615
diff changeset
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
afddfebea797 t0f=t0 done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 612
diff changeset
147 TMap (t0 lim) i o (limit (isLimit lim) b (ta a x t ) o id1 A b )
afddfebea797 t0f=t0 done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 612
diff changeset
148 ≈⟨ cdr idR ⟩
afddfebea797 t0f=t0 done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 612
diff changeset
149 TMap (t0 lim) i o limit (isLimit lim) b (ta a x t )
afddfebea797 t0f=t0 done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 612
diff changeset
150 ≈⟨ t0f=t (isLimit lim) ⟩
afddfebea797 t0f=t0 done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 612
diff changeset
151 TMap (ta a x t) i
afddfebea797 t0f=t0 done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 612
diff changeset
152 ≈⟨⟩
612
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 611
diff changeset
153 TMap t i x
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 611
diff changeset
154 ∎ ))
616
7011165c118e on going ..
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 615
diff changeset
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))} →
7011165c118e on going ..
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 615
diff changeset
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
7011165c118e on going ..
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 615
diff changeset
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
3fb4d834c349 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 609
diff changeset
169
609
d686d7ae38e0 on goging
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 608
diff changeset
170
d686d7ae38e0 on goging
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 608
diff changeset
171 UpreserveLimit : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (I : Category c₁ c₂ ℓ)
616
7011165c118e on going ..
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 615
diff changeset
172 (b : Obj A ) → LimitPreserve A I Sets (Yoneda A b)
612
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 611
diff changeset
173 UpreserveLimit A I b = record {
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 611
diff changeset
174 preserve = λ Γ lim → UpreserveLimit0 A I b Γ lim
610
3fb4d834c349 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 609
diff changeset
175 }
609
d686d7ae38e0 on goging
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 608
diff changeset
176
624
9b9bc1e076f3 introduce one element set
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 623
diff changeset
177
608
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 502
diff changeset
178 -- K{*}↓U has preinitial full subcategory if U is representable
609
d686d7ae38e0 on goging
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 608
diff changeset
179 -- if U is representable, K{*}↓U has initial Object ( so it has preinitial full subcategory )
608
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 502
diff changeset
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
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 626
diff changeset
183 data * {c : Level} : Set c where
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 626
diff changeset
184 OneObj : *
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 626
diff changeset
185
609
d686d7ae38e0 on goging
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 608
diff changeset
186 KUhasInitialObj : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ)
608
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 502
diff changeset
187 (a : Obj A )
628
b99660fa14e1 remove arrow's yellow
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 627
diff changeset
188 → HasInitialObject ( K (Sets) A * ↓ (Yoneda A a) ) ( record { obj = a ; hom = λ x → id1 A a } )
621
19f31d22e790 add desciptive lemma
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 620
diff changeset
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
19f31d22e790 add desciptive lemma
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 620
diff changeset
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
d73fbed639a9 initialObject done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 624
diff changeset
220 -- what is comm f ?
d73fbed639a9 initialObject done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 624
diff changeset
221 comm-f : (b : Obj (K Sets A * ↓ (Yoneda A a))) (f : Hom (K Sets A * ↓ Yoneda A a) initObj b)
d73fbed639a9 initialObject done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 624
diff changeset
222 → Sets [ Sets [ FMap (Yoneda A a) (arrow f) o ( λ x → id1 A a ) ]
d73fbed639a9 initialObject done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 624
diff changeset
223 ≈ Sets [ hom b o FMap (K Sets A *) (arrow f) ] ]
d73fbed639a9 initialObject done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 624
diff changeset
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
d73fbed639a9 initialObject done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 624
diff changeset
233 ≈⟨⟩
d73fbed639a9 initialObject done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 624
diff changeset
234 ( Sets [ FMap (Yoneda A a) (arrow f) o ( λ x → id1 A a ) ] ) OneObj
d73fbed639a9 initialObject done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 624
diff changeset
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
633
37fa9d3fab8c add equalizer
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 632
diff changeset
243 -- A is complete and K{*}↓U has preinitial full subcategory then U is representable
615
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
c5abbd39e6eb on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 625
diff changeset
247
c5abbd39e6eb on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 625
diff changeset
248 ≡-cong = Relation.Binary.PropositionalEquality.cong
c5abbd39e6eb on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 625
diff changeset
249
632
d36ff598a063 add compleness
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 631
diff changeset
250 UisRepresentable : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) ( comp : Complete A A )
626
c5abbd39e6eb on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 625
diff changeset
251 (U : Functor A (Sets {c₂}) )
628
b99660fa14e1 remove arrow's yellow
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 627
diff changeset
252 (SFS : SmallFullSubcategory ( K (Sets {c₂}) A * ↓ U) )
629
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 628
diff changeset
253 (PI : PreInitial ( K (Sets) A * ↓ U) (SFSF SFS))
626
c5abbd39e6eb on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 625
diff changeset
254 → Representable A U (obj (preinitialObj PI ))
632
d36ff598a063 add compleness
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 631
diff changeset
255 UisRepresentable A comp U SFS PI = record {
627
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 626
diff changeset
256 repr→ = record { TMap = tmap1 ; isNTrans = record { commute = comm1 } }
626
c5abbd39e6eb on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 625
diff changeset
257 ; repr← = record { TMap = tmap2 ; isNTrans = record { commute = comm2 } }
628
b99660fa14e1 remove arrow's yellow
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 627
diff changeset
258 ; reprId→ = {!!}
b99660fa14e1 remove arrow's yellow
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 627
diff changeset
259 ; reprId← = {!!}
626
c5abbd39e6eb on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 625
diff changeset
260 } where
629
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 628
diff changeset
261 pi : Obj ( K (Sets) A * ↓ U)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 628
diff changeset
262 pi = preinitialObj PI
630
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 629
diff changeset
263 pihom : Hom Sets (FObj (K Sets A *) (obj pi)) (FObj U (obj pi))
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 629
diff changeset
264 pihom = hom pi
629
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 628
diff changeset
265 ub : (b : Obj A) (x : FObj U b ) → Hom Sets (FObj (K Sets A *) b) (FObj U b)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 628
diff changeset
266 ub b x OneObj = x
630
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 629
diff changeset
267 ob : (b : Obj A) (x : FObj U b ) → Obj ( K Sets A * ↓ U)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 629
diff changeset
268 ob b x = record { obj = b ; hom = ub b x}
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 629
diff changeset
269 piArrow : (b : Obj ( K Sets A * ↓ U)) → Hom ( K Sets A * ↓ U) pi b
631
7be3eb96310c introduce fArrow
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 630
diff changeset
270 piArrow b = SFSFMap← SFS ( preinitialArrow PI {FObj (SFSF SFS) b} )
7be3eb96310c introduce fArrow
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 630
diff changeset
271 fArrowComm1 : (a b : Obj A) (f : Hom A a b) (x : FObj U a ) → (y : * ) → FMap U f ( ub a x y ) ≡ ub b (FMap U f x) y
632
d36ff598a063 add compleness
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 631
diff changeset
272 fArrowComm1 a b f x OneObj = refl
631
7be3eb96310c introduce fArrow
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 630
diff changeset
273 fArrowComm : (a b : Obj A) (f : Hom A a b) (x : FObj U a ) →
7be3eb96310c introduce fArrow
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 630
diff changeset
274 Sets [ Sets [ FMap U f o hom (ob a x) ] ≈ Sets [ hom (ob b (FMap U f x)) o FMap (K Sets A *) f ] ]
7be3eb96310c introduce fArrow
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 630
diff changeset
275 fArrowComm a b f x = extensionality Sets ( λ y → begin
7be3eb96310c introduce fArrow
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 630
diff changeset
276 ( Sets [ FMap U f o hom (ob a x) ] ) y
7be3eb96310c introduce fArrow
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 630
diff changeset
277 ≡⟨⟩
7be3eb96310c introduce fArrow
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 630
diff changeset
278 FMap U f ( hom (ob a x) y )
7be3eb96310c introduce fArrow
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 630
diff changeset
279 ≡⟨⟩
7be3eb96310c introduce fArrow
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 630
diff changeset
280 FMap U f ( ub a x y )
7be3eb96310c introduce fArrow
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 630
diff changeset
281 ≡⟨ fArrowComm1 a b f x y ⟩
7be3eb96310c introduce fArrow
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 630
diff changeset
282 ub b (FMap U f x) y
7be3eb96310c introduce fArrow
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 630
diff changeset
283 ≡⟨⟩
7be3eb96310c introduce fArrow
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 630
diff changeset
284 hom (ob b (FMap U f x)) y
7be3eb96310c introduce fArrow
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 630
diff changeset
285 ≡⟨⟩
7be3eb96310c introduce fArrow
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 630
diff changeset
286 ( Sets [ hom (ob b (FMap U f x)) o FMap (K Sets A *) f ] ) y
7be3eb96310c introduce fArrow
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 630
diff changeset
287 ∎ ) where
7be3eb96310c introduce fArrow
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 630
diff changeset
288 open import Relation.Binary.PropositionalEquality
7be3eb96310c introduce fArrow
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 630
diff changeset
289 open ≡-Reasoning
7be3eb96310c introduce fArrow
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 630
diff changeset
290 fArrow : (a b : Obj A) (f : Hom A a b) (x : FObj U a ) → Hom ( K Sets A * ↓ U) ( ob a x ) (ob b (FMap U f x) )
7be3eb96310c introduce fArrow
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 630
diff changeset
291 fArrow a b f x = record { arrow = f ; comm = fArrowComm a b f x }
630
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 629
diff changeset
292 preinitComm : (a : Obj A ) ( x : FObj U a ) → Sets [ Sets [ FMap U (arrow (piArrow (ob a x))) o hom pi ]
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 629
diff changeset
293 ≈ Sets [ ub a x o FMap (K Sets A *) (arrow (piArrow (ob a x))) ] ]
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 629
diff changeset
294 preinitComm a x = comm (piArrow (ob a x ))
633
37fa9d3fab8c add equalizer
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 632
diff changeset
295 equ : {a b : Obj A} → (f g : Hom A a b) → IsEqualizer A (equalizer-e comp f g ) f g
37fa9d3fab8c add equalizer
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 632
diff changeset
296 equ f g = Complete.isEqualizer comp f g
37fa9d3fab8c add equalizer
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 632
diff changeset
297 ep : {a b : Obj A} → {f g : Hom A a b} → Obj A
37fa9d3fab8c add equalizer
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 632
diff changeset
298 ep {a} {b} {f} {g} = equalizer-p comp f g
37fa9d3fab8c add equalizer
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 632
diff changeset
299 ee : {a b : Obj A} → {f g : Hom A a b} → Hom A (ep {a} {b} {f} {g} ) a
37fa9d3fab8c add equalizer
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 632
diff changeset
300 ee {a} {b} {f} {g} = equalizer-e comp f g
37fa9d3fab8c add equalizer
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 632
diff changeset
301 preinitialEqu : {x y : Obj ( K (Sets) A * ↓ U) } → (f : Hom ( K (Sets) A * ↓ U) x y ) →
634
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 633
diff changeset
302 IsEqualizer A ee (A [ arrow f o arrow ( preinitialArrow PI {x}) ] ) ( arrow ( preinitialArrow PI {y}) )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 633
diff changeset
303 preinitialEqu {x} {y} f = Complete.isEqualizer comp ( A [ arrow f o arrow (preinitialArrow PI) ] ) ( arrow ( preinitialArrow PI ))
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 633
diff changeset
304 pa : {x y : Obj ( K (Sets) A * ↓ U) } → (f : Hom ( K (Sets) A * ↓ U) x y )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 633
diff changeset
305 → Hom ( K (Sets) A * ↓ U) (preinitialObj PI)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 633
diff changeset
306 (ob (Complete.equalizer-p comp ( A [ arrow f o arrow (preinitialArrow PI) ] ) ( arrow ( preinitialArrow PI ))) {!!} )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 633
diff changeset
307 pa {x} {y} f = piArrow (ob (Complete.equalizer-p comp ( A [ arrow f o arrow (preinitialArrow PI) ] ) ( arrow ( preinitialArrow PI ))) {!!} )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 633
diff changeset
308 --
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 633
diff changeset
309 -- e f
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 633
diff changeset
310 -- c -------→ a ---------→ b
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 633
diff changeset
311 -- ^ . ---------→
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 633
diff changeset
312 -- | . g
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 633
diff changeset
313 -- |k .
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 633
diff changeset
314 -- | . h
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 633
diff changeset
315 -- d
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 633
diff changeset
316 --
632
d36ff598a063 add compleness
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 631
diff changeset
317 comm13 : (a b : Obj ( K Sets A * ↓ U)) (f : Hom ( K Sets A * ↓ U) a b ) → ( K Sets A * ↓ U) [
d36ff598a063 add compleness
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 631
diff changeset
318 ( K Sets A * ↓ U) [ f o preinitialArrow PI ] ≈ preinitialArrow PI ]
d36ff598a063 add compleness
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 631
diff changeset
319 comm13 a b f = let open ≈-Reasoning A in begin
d36ff598a063 add compleness
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 631
diff changeset
320 arrow ( ( K Sets A * ↓ U) [ f o preinitialArrow PI ] )
d36ff598a063 add compleness
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 631
diff changeset
321 ≈⟨⟩
633
37fa9d3fab8c add equalizer
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 632
diff changeset
322 arrow f o arrow ( preinitialArrow PI {{!!}})
632
d36ff598a063 add compleness
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 631
diff changeset
323 ≈⟨ {!!} ⟩
633
37fa9d3fab8c add equalizer
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 632
diff changeset
324 arrow ( preinitialArrow PI {{!!}} )
634
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 633
diff changeset
325 ∎
632
d36ff598a063 add compleness
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 631
diff changeset
326 comm12 : (a b : Obj A) (f : Hom A a b) (y : FObj U a ) → ( K Sets A * ↓ U) [
d36ff598a063 add compleness
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 631
diff changeset
327 FMap (SFSF SFS) ( ( K Sets A * ↓ U) [ fArrow a b f y o (piArrow (ob a y)) ] ) ≈ FMap (SFSF SFS) ( piArrow (ob b (FMap U f y ))) ]
d36ff598a063 add compleness
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 631
diff changeset
328 comm12 a b f y = let open ≈-Reasoning ( K Sets A * ↓ U) in begin
d36ff598a063 add compleness
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 631
diff changeset
329 FMap (SFSF SFS) ( ( K Sets A * ↓ U) [ fArrow a b f y o (piArrow (ob a y)) ] )
d36ff598a063 add compleness
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 631
diff changeset
330 ≈⟨ {!!} ⟩
d36ff598a063 add compleness
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 631
diff changeset
331 FMap (SFSF SFS) ( fArrow a b f y ) o FMap (SFSF SFS) ( piArrow (ob a y))
d36ff598a063 add compleness
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 631
diff changeset
332 ≈⟨ {!!} ⟩
d36ff598a063 add compleness
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 631
diff changeset
333 FMap (SFSF SFS) ( fArrow a b f y ) o preinitialArrow PI {FObj (SFSF SFS) (ob a y ) }
d36ff598a063 add compleness
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 631
diff changeset
334 ≈⟨ comm13 (FObj (SFSF SFS) (ob a y)) (FObj (SFSF SFS) (ob b (FMap U f y))) (FMap (SFSF SFS) (fArrow a b f y)) ⟩
d36ff598a063 add compleness
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 631
diff changeset
335 preinitialArrow PI {FObj (SFSF SFS) (ob b (FMap U f y )) }
d36ff598a063 add compleness
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 631
diff changeset
336 ≈⟨ {!!} ⟩
d36ff598a063 add compleness
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 631
diff changeset
337 FMap (SFSF SFS) ( piArrow (ob b (FMap U f y )))
d36ff598a063 add compleness
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 631
diff changeset
338 ∎
629
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 628
diff changeset
339 comm11 : (a b : Obj A) (f : Hom A a b) (y : FObj U a ) →
630
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 629
diff changeset
340 ( Sets [ FMap (Yoneda A (obj (preinitialObj PI))) f o ( λ x → arrow (piArrow (ob a x))) ] ) y
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 629
diff changeset
341 ≡ (Sets [ ( λ x → arrow (piArrow (ob b x))) o FMap U f ] ) y
629
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 628
diff changeset
342 comm11 a b f y = begin
630
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 629
diff changeset
343 ( Sets [ FMap (Yoneda A (obj (preinitialObj PI))) f o ( λ x → arrow (piArrow (ob a x))) ] ) y
629
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 628
diff changeset
344 ≡⟨⟩
630
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 629
diff changeset
345 A [ f o arrow (piArrow (ob a y)) ]
631
7be3eb96310c introduce fArrow
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 630
diff changeset
346 ≡⟨⟩
7be3eb96310c introduce fArrow
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 630
diff changeset
347 A [ arrow ( fArrow a b f y ) o arrow (piArrow (ob a y)) ]
7be3eb96310c introduce fArrow
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 630
diff changeset
348 ≡⟨⟩
7be3eb96310c introduce fArrow
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 630
diff changeset
349 arrow ( ( K Sets A * ↓ U) [ ( fArrow a b f y ) o (piArrow (ob a y)) ] )
629
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 628
diff changeset
350 ≡⟨ {!!} ⟩
632
d36ff598a063 add compleness
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 631
diff changeset
351 arrow ( ( SFSFMap← SFS ) ( FMap (SFSF SFS) ( ( K Sets A * ↓ U) [ ( fArrow a b f y ) o (piArrow (ob a y)) ] ) ) )
d36ff598a063 add compleness
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 631
diff changeset
352 ≡⟨ ≡-cong ( λ k → arrow ( (SFSFMap← SFS ) k )) ( ≈-≡ ( K Sets A * ↓ U) ( comm12 a b f y ) ) ⟩
d36ff598a063 add compleness
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 631
diff changeset
353 arrow ( ( SFSFMap← SFS ) ( FMap (SFSF SFS) ( piArrow (ob b (FMap U f y) ) )) )
d36ff598a063 add compleness
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 631
diff changeset
354 ≡⟨ {!!} ⟩
630
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 629
diff changeset
355 arrow (piArrow (ob b (FMap U f y) ))
629
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 628
diff changeset
356 ≡⟨⟩
630
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 629
diff changeset
357 (Sets [ ( λ x → arrow (piArrow (ob b x))) o FMap U f ] ) y
629
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 628
diff changeset
358 ∎ where
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 628
diff changeset
359 open import Relation.Binary.PropositionalEquality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 628
diff changeset
360 open ≡-Reasoning
632
d36ff598a063 add compleness
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 631
diff changeset
361 tmap1 : (b : Obj A) → Hom Sets (FObj U b) (FObj (Yoneda A (obj pi)) b)
d36ff598a063 add compleness
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 631
diff changeset
362 tmap1 b x = arrow ( piArrow ( ob b x ) )
626
c5abbd39e6eb on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 625
diff changeset
363 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 ] ]
c5abbd39e6eb on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 625
diff changeset
364 comm1 {a} {b} {f} = let open ≈-Reasoning Sets in begin
c5abbd39e6eb on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 625
diff changeset
365 FMap (Yoneda A (obj (preinitialObj PI))) f o tmap1 a
629
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 628
diff changeset
366 ≈⟨⟩
630
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 629
diff changeset
367 FMap (Yoneda A (obj (preinitialObj PI))) f o ( λ x → arrow (piArrow ( ob a x )))
629
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 628
diff changeset
368 ≈⟨ extensionality Sets ( λ y → comm11 a b f y ) ⟩
630
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 629
diff changeset
369 ( λ x → arrow (piArrow (ob b x))) o FMap U f
629
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 628
diff changeset
370 ≈⟨⟩
626
c5abbd39e6eb on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 625
diff changeset
371 tmap1 b o FMap U f
c5abbd39e6eb on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 625
diff changeset
372 ∎
c5abbd39e6eb on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 625
diff changeset
373 comm21 : (a b : Obj A) (f : Hom A a b) ( y : Hom A (obj (preinitialObj PI)) a ) →
c5abbd39e6eb on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 625
diff changeset
374 (Sets [ FMap U f o (λ x → FMap U x (hom (preinitialObj PI) OneObj))] ) y ≡
c5abbd39e6eb on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 625
diff changeset
375 (Sets [ ( λ x → (FMap U x ) (hom (preinitialObj PI) OneObj)) o (λ x → A [ f o x ] ) ] ) y
c5abbd39e6eb on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 625
diff changeset
376 comm21 a b f y = begin
c5abbd39e6eb on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 625
diff changeset
377 FMap U f ( FMap U y (hom (preinitialObj PI) OneObj))
c5abbd39e6eb on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 625
diff changeset
378 ≡⟨ ≡-cong ( λ k → k (hom (preinitialObj PI) OneObj)) ( sym ( IsFunctor.distr (isFunctor U ) ) ) ⟩
c5abbd39e6eb on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 625
diff changeset
379 (FMap U (A [ f o y ] ) ) (hom (preinitialObj PI) OneObj)
c5abbd39e6eb on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 625
diff changeset
380 ∎ where
c5abbd39e6eb on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 625
diff changeset
381 open import Relation.Binary.PropositionalEquality
c5abbd39e6eb on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 625
diff changeset
382 open ≡-Reasoning
630
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 629
diff changeset
383 tmap2 : (b : Obj A) → Hom Sets (FObj (Yoneda A (obj (preinitialObj PI))) b) (FObj U b)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 629
diff changeset
384 tmap2 b x = ( FMap U x ) ( hom ( preinitialObj PI ) OneObj )
626
c5abbd39e6eb on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 625
diff changeset
385 comm2 : {a b : Obj A} {f : Hom A a b} → Sets [ Sets [ FMap U f o tmap2 a ] ≈
c5abbd39e6eb on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 625
diff changeset
386 Sets [ tmap2 b o FMap (Yoneda A (obj (preinitialObj PI))) f ] ]
c5abbd39e6eb on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 625
diff changeset
387 comm2 {a} {b} {f} = let open ≈-Reasoning Sets in begin
c5abbd39e6eb on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 625
diff changeset
388 FMap U f o tmap2 a
c5abbd39e6eb on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 625
diff changeset
389 ≈⟨⟩
c5abbd39e6eb on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 625
diff changeset
390 FMap U f o ( λ x → ( FMap U x ) ( hom ( preinitialObj PI ) OneObj ) )
c5abbd39e6eb on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 625
diff changeset
391 ≈⟨ extensionality Sets ( λ y → comm21 a b f y ) ⟩
c5abbd39e6eb on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 625
diff changeset
392 ( λ x → ( FMap U x ) ( hom ( preinitialObj PI ) OneObj ) ) o ( λ x → A [ f o x ] )
c5abbd39e6eb on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 625
diff changeset
393 ≈⟨⟩
c5abbd39e6eb on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 625
diff changeset
394 ( λ x → ( FMap U x ) ( hom ( preinitialObj PI ) OneObj ) ) o FMap (Yoneda A (obj (preinitialObj PI))) f
c5abbd39e6eb on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 625
diff changeset
395 ≈⟨⟩
c5abbd39e6eb on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 625
diff changeset
396 tmap2 b o FMap (Yoneda A (obj (preinitialObj PI))) f
c5abbd39e6eb on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 625
diff changeset
397 ∎