Mercurial > hg > Members > kono > Proof > category

annotate src/freyd2.agda @ 949:ac53803b3b2a

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