Mercurial > hg > Members > kono > Proof > category

annotate freyd2.agda @ 623:bed3be9a4168

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
One
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Fri, 23 Jun 2017 19:11:36 +0900
parents bd890a43ef5b
children 9b9bc1e076f3
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
e8b85a05a6b2 add if U is iso to representable functor then preserve limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
27 ----
e8b85a05a6b2 add if U is iso to representable functor then preserve limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
28 --
617
34540494fdcf initital obj uniquness done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 616
diff changeset
29 -- 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
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
e8b85a05a6b2 add if U is iso to representable functor then preserve limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
33 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
34 open Functor
498
c981a2f0642f UpreseveLimit detailing
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 497
diff changeset
35 open Limit
c981a2f0642f UpreseveLimit detailing
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 497
diff changeset
36 open IsLimit
c981a2f0642f UpreseveLimit detailing
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 497
diff changeset
37 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
38
616
7011165c118e on going ..
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 615
diff changeset
39 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
40 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
41 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
42 ; 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
43 ; 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
44 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
45 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
46 ≈-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
47 }
e8b85a05a6b2 add if U is iso to representable functor then preserve limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
48 } where
e8b85a05a6b2 add if U is iso to representable functor then preserve limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
49 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
50 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
51 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
52 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
53 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
54 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
55 ≈↑⟨ assoc ⟩
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 [ 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
57 ≈⟨⟩
e8b85a05a6b2 add if U is iso to representable functor then preserve limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
58 ( λ 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
59 ∎ )
e8b85a05a6b2 add if U is iso to representable functor then preserve limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
60 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
61 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
62 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
63 ≈⟨ 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
64 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
65 ∎ )
e8b85a05a6b2 add if U is iso to representable functor then preserve limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
66
609
d686d7ae38e0 on goging
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 608
diff changeset
67 -- Representable U ≈　Hom(A,-)
502
01a0dda67a8b on going ..
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 499
diff changeset
68
609
d686d7ae38e0 on goging
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 608
diff changeset
69 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
70 field
01a0dda67a8b on going ..
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 499
diff changeset
71 -- FObj U x : A → Set
609
d686d7ae38e0 on goging
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 608
diff changeset
72 -- FMap U f = Set → Set (locally small)
502
01a0dda67a8b on going ..
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 499
diff changeset
73 -- λ b → Hom (a,b) : A → Set
01a0dda67a8b on going ..
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 499
diff changeset
74 -- λ f → Hom (a,-) = λ b → Hom a b
01a0dda67a8b on going ..
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 499
diff changeset
75
616
7011165c118e on going ..
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 615
diff changeset
76 repr→ : NTrans A (Sets {c₂}) U (Yoneda A a )
7011165c118e on going ..
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 615
diff changeset
77 repr← : NTrans A (Sets {c₂}) (Yoneda A a) U
7011165c118e on going ..
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 615
diff changeset
78 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
79 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
80
609
d686d7ae38e0 on goging
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 608
diff changeset
81 open Representable
608
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 502
diff changeset
82 open import freyd
502
01a0dda67a8b on going ..
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 499
diff changeset
83
609
d686d7ae38e0 on goging
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 608
diff changeset
84 open LimitPreserve
608
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 502
diff changeset
85
609
d686d7ae38e0 on goging
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 608
diff changeset
86 -- 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
87 --
616
7011165c118e on going ..
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 615
diff changeset
88 -- 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
89 -- : Functor Sets A
610
3fb4d834c349 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 609
diff changeset
90
3fb4d834c349 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 609
diff changeset
91 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
92 (b : Obj A )
610
3fb4d834c349 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 609
diff changeset
93 (Γ : Functor I A) (limita : Limit A I Γ) →
616
7011165c118e on going ..
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 615
diff changeset
94 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
95 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
96 limit = λ a t → ψ a t
b1b5c6b4c570 natural transformation in representable functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 610
diff changeset
97 ; 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
98 ; 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
99 } where
616
7011165c118e on going ..
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 615
diff changeset
100 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
101 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
102 haa0 : Obj Sets
616
7011165c118e on going ..
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 615
diff changeset
103 haa0 = FObj (Yoneda A b) (a0 lim)
7011165c118e on going ..
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 615
diff changeset
104 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
105 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
106 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
107 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
108 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
109 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
110 ≈⟨⟩
616
7011165c118e on going ..
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 615
diff changeset
111 ( ( 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
112 ≈⟨ ≡-≈ ( 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
113 ( 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
114 ≈⟨⟩
b1b5c6b4c570 natural transformation in representable functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 610
diff changeset
115 ( 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
116 ≈⟨⟩
b1b5c6b4c570 natural transformation in representable functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 610
diff changeset
117 TMap t b₁ x
b1b5c6b4c570 natural transformation in representable functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 610
diff changeset
118 ≈↑⟨ idR ⟩
b1b5c6b4c570 natural transformation in representable functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 610
diff changeset
119 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
120 ≈⟨⟩
b1b5c6b4c570 natural transformation in representable functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 610
diff changeset
121 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 ∎
616
7011165c118e on going ..
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 615
diff changeset
123 ψ : (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
124 → Hom Sets X (FObj (Yoneda A b) (a0 lim))
7011165c118e on going ..
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 615
diff changeset
125 ψ 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
126 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
127 → 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
128 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
129 ( 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
130 ≈⟨⟩
616
7011165c118e on going ..
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 615
diff changeset
131 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
132 ≈⟨⟩ -- 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
133 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
134 ≈⟨ cdr idR ⟩
afddfebea797 t0f=t0 done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 612
diff changeset
135 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
136 ≈⟨ t0f=t (isLimit lim) ⟩
afddfebea797 t0f=t0 done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 612
diff changeset
137 TMap (ta a x t) i
afddfebea797 t0f=t0 done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 612
diff changeset
138 ≈⟨⟩
612
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 611
diff changeset
139 TMap t i x
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 611
diff changeset
140 ∎ ))
616
7011165c118e on going ..
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 615
diff changeset
141 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
142 ({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
143 Sets [ ψ a t ≈ f ]
e6be03d94284 Representational Functor preserve limit done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 613
diff changeset
144 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
145 ψ a t x
e6be03d94284 Representational Functor preserve limit done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 613
diff changeset
146 ≈⟨⟩
616
7011165c118e on going ..
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 615
diff changeset
147 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
148 ≈⟨⟩
e6be03d94284 Representational Functor preserve limit done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 613
diff changeset
149 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
150 ≈⟨ idR ⟩
e6be03d94284 Representational Functor preserve limit done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 613
diff changeset
151 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
152 ≈⟨ 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
153 f x
e6be03d94284 Representational Functor preserve limit done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 613
diff changeset
154 ∎ ))
610
3fb4d834c349 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 609
diff changeset
155
609
d686d7ae38e0 on goging
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 608
diff changeset
156
d686d7ae38e0 on goging
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 608
diff changeset
157 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
158 (b : Obj A ) → LimitPreserve A I Sets (Yoneda A b)
612
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 611
diff changeset
159 UpreserveLimit A I b = record {
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 611
diff changeset
160 preserve = λ Γ lim → UpreserveLimit0 A I b Γ lim
610
3fb4d834c349 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 609
diff changeset
161 }
609
d686d7ae38e0 on goging
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 608
diff changeset
162
608
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 502
diff changeset
163 -- 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
164 -- 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
165
623
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 622
diff changeset
166 data OneObject {c : Level} : Set c where
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 622
diff changeset
167 OneObj : OneObject
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 622
diff changeset
168
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 622
diff changeset
169 data OneMor {c : Level} : OneObject {c} → OneObject {c} → Set c where
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 622
diff changeset
170 OneIdMor : OneMor OneObj OneObj
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 622
diff changeset
171
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 622
diff changeset
172 comp : {A B C : OneObject} → OneMor B C → OneMor A B → OneMor A C
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 622
diff changeset
173 comp OneIdMor OneIdMor = OneIdMor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 622
diff changeset
174
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 622
diff changeset
175 OneEquiv : {c : Level} {A B : OneObject {c} } → IsEquivalence {c} {c} {OneMor A B} _≡_
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 622
diff changeset
176 OneEquiv = record { refl = refl ; sym = ≡-sym; trans = ≡-trans}
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 622
diff changeset
177
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 622
diff changeset
178 OneID : {A : OneObject} → OneMor A A
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 622
diff changeset
179 OneID {OneObj} = OneIdMor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 622
diff changeset
180
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 622
diff changeset
181 OneAssoc : {A B C D : OneObject} {f : OneMor C D} {g : OneMor B C } {h : OneMor A B}
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 622
diff changeset
182 → comp f (comp g h) ≡ comp (comp f g) h
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 622
diff changeset
183 OneAssoc {OneObj} {OneObj} {OneObj} {OneObj} {OneIdMor} {OneIdMor} {OneIdMor} = refl
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 622
diff changeset
184
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 622
diff changeset
185 OneIdentityL : {A B : OneObject} {f : OneMor A B} → (comp OneID f) ≡ f
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 622
diff changeset
186 OneIdentityL {OneObj} {OneObj} {OneIdMor} = refl
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 622
diff changeset
187
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 622
diff changeset
188 OneIdentityR : {A B : OneObject} {f : OneMor A B} → (comp f OneID) ≡ f
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 622
diff changeset
189 OneIdentityR {OneObj} {OneObj} {OneIdMor} = refl
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 622
diff changeset
190
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 622
diff changeset
191 o-resp-≡ : {A B C : OneObject} {f g : OneMor A B} {h i : OneMor B C} → f ≡ g → h ≡ i → comp h f ≡ comp i g
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 622
diff changeset
192 o-resp-≡ {OneObj} {OneObj} {OneObj} {f} {g} {h} {i} f≡g h≡i =
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 622
diff changeset
193 ≡-trans (cong (comp h) f≡g) (cong (λ x → comp x g) h≡i)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 622
diff changeset
194
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 622
diff changeset
195
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 622
diff changeset
196 isCategory : { c : Level } → IsCategory {c} {c} {c} OneObject OneMor _≡_ comp OneID
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 622
diff changeset
197 isCategory = record { isEquivalence = OneEquiv
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 622
diff changeset
198 ; identityL = OneIdentityL
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 622
diff changeset
199 ; identityR = OneIdentityR
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 622
diff changeset
200 ; o-resp-≈ = o-resp-≡
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 622
diff changeset
201 ; associative = OneAssoc
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 622
diff changeset
202 }
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 622
diff changeset
203
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 622
diff changeset
204 ONE : { c : Level } → Category c c c
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 622
diff changeset
205 ONE = record { Obj = OneObject
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 622
diff changeset
206 ; Hom = OneMor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 622
diff changeset
207 ; _≈_ = _≡_
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 622
diff changeset
208 ; Id = OneID
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 622
diff changeset
209 ; isCategory = isCategory
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 622
diff changeset
210 }
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 622
diff changeset
211
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 622
diff changeset
212 _↓_ : { c₁ c₂ ℓ c₁' c₂' ℓ' c₁'' c₂'' ℓ'' : Level} { A : Category c₁ c₂ ℓ } { B : Category c₁' c₂' ℓ' } { C : Category c₁'' c₂'' ℓ'' }
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 622
diff changeset
213 → ( F : Functor A C )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 622
diff changeset
214 → ( G : Functor B C )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 622
diff changeset
215 → Category (c₂'' ⊔ c₁ ⊔ c₁') (ℓ'' ⊔ c₂ ⊔ c₂') ( ℓ ⊔ ℓ' )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 622
diff changeset
216 _↓_ { c₁} {c₂} {ℓ} {c₁'} {c₂'} {ℓ'} {c₁''} {c₂''} {ℓ''} {A} {B} {C} F G = CommaCategory
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 622
diff changeset
217 where open import Comma F G
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 622
diff changeset
218
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 622
diff changeset
219 open import freyd
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 622
diff changeset
220 open SmallFullSubcategory
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 622
diff changeset
221 open Complete
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 622
diff changeset
222 open PreInitial
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 622
diff changeset
223 open HasInitialObject
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 622
diff changeset
224 open import Comma
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 622
diff changeset
225 open CommaObj
617
34540494fdcf initital obj uniquness done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 616
diff changeset
226 open CommaHom
34540494fdcf initital obj uniquness done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 616
diff changeset
227
609
d686d7ae38e0 on goging
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 608
diff changeset
228 KUhasInitialObj : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ)
608
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 502
diff changeset
229 (a : Obj A )
623
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 622
diff changeset
230 → HasInitialObject {c₁} {c₂} {ℓ} ( K Sets ONE OneObject ↓ (Yoneda A a) ) ( record { obj = OneObj ; hom = {!!} } )
621
19f31d22e790 add desciptive lemma
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 620
diff changeset
231 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
232 initial = λ b → initial0 b
623
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 622
diff changeset
233 ; uniqueness = {!!}
615
a45c32ceca97 initial Object's arrow found
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 614
diff changeset
234 } where
621
19f31d22e790 add desciptive lemma
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 620
diff changeset
235 commaCat : Category (c₂ ⊔ c₁) c₂ ℓ
623
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 622
diff changeset
236 commaCat = K Sets ONE OneObject ↓ Yoneda A a
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 622
diff changeset
237 initObj : Obj (K Sets ONE OneObject ↓ Yoneda A a)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 622
diff changeset
238 initObj = record { obj = OneObj ; hom = {!!} }
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 622
diff changeset
239 initial0comm1 : (b : Obj (K Sets ONE OneObject ↓ (Yoneda A a))) → (x : {!!} )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 622
diff changeset
240 → FMap (Yoneda A a) (hom b {!!}) x ≡ hom b {!!}
618
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 617
diff changeset
241 initial0comm1 b x = let open ≈-Reasoning A in ≈-≡ A ( begin
623
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 622
diff changeset
242 FMap (Yoneda A a) (hom b {!!}) x
615
a45c32ceca97 initial Object's arrow found
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 614
diff changeset
243 ≈⟨⟩
623
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 622
diff changeset
244 hom b {!!} o x
620
c95add5b7cbe on going ..
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 619
diff changeset
245 ≈⟨ {!!} ⟩
623
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 622
diff changeset
246 hom b {!!}
616
7011165c118e on going ..
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 615
diff changeset
247 ∎ )
623
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 622
diff changeset
248 initial0comm : (b : Obj (K Sets ONE OneObject ↓ (Yoneda A a))) →
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 622
diff changeset
249 Sets [ Sets [ FMap (Yoneda A a) (hom b {!!}) o id1 Sets (FObj (Yoneda A a) a) ] ≈ {!!} ]
618
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 617
diff changeset
250 initial0comm b = let open ≈-Reasoning Sets in begin
623
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 622
diff changeset
251 FMap (Yoneda A a) (hom b {!!}) o id1 Sets (FObj (Yoneda A a) a)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 622
diff changeset
252 ≈⟨ {!!} ⟩
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 622
diff changeset
253 {!!}
615
a45c32ceca97 initial Object's arrow found
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 614
diff changeset
254 ∎
623
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 622
diff changeset
255 initial0 : (b : Obj (K Sets ONE OneObject ↓ (Yoneda A a))) →
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 622
diff changeset
256 Hom (K Sets ONE OneObject ↓ (Yoneda A a)) initObj b
615
a45c32ceca97 initial Object's arrow found
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 614
diff changeset
257 initial0 b = record {
623
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 622
diff changeset
258 arrow = {!!}
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 622
diff changeset
259 ; comm = {!!} }
615
a45c32ceca97 initial Object's arrow found
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 614
diff changeset
260
a45c32ceca97 initial Object's arrow found
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 614
diff changeset
261
a45c32ceca97 initial Object's arrow found
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 614
diff changeset
262 -- K{*}↓U has preinitial full subcategory then U is representable
a45c32ceca97 initial Object's arrow found
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 614
diff changeset
263
617
34540494fdcf initital obj uniquness done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 616
diff changeset
264 open SmallFullSubcategory
34540494fdcf initital obj uniquness done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 616
diff changeset
265 open PreInitial
622
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 621
diff changeset
266 --
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 621
diff changeset
267 -- UisRepresentable : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 621
diff changeset
268 -- (U : Functor A (Sets {c₂}) )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 621
diff changeset
269 -- (a : Obj (Sets {c₂})) (ax : a)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 621
diff changeset
270 -- (SFS : SmallFullSubcategory {c₁} {c₂} {ℓ} ( K (Sets {c₂}) A a ↓ U) )
623
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 622
diff changeset
271 -- (PI : PreInitial {c₁} {c₂} {ℓ} ( K Sets ONE OneObject ↓ U) (SFSF SFS ))
622
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 621
diff changeset
272 -- → Representable A U (obj (preinitialObj PI ))
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 621
diff changeset
273 -- UisRepresentable A U a ax SFS PI = record {
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 621
diff changeset
274 -- repr→ = record { TMap = tmap1 ; isNTrans = record { commute = {!!} } }
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 621
diff changeset
275 -- ; repr← = record { TMap = tmap2 ; isNTrans = record { commute = {!!} } }
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 621
diff changeset
276 -- ; reprId→ = λ {y} →　?
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 621
diff changeset
277 -- ; reprId← = λ {y} →　?
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 621
diff changeset
278 -- } where
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 621
diff changeset
279 -- tmap1 : (b : Obj A) → Hom Sets (FObj U b) (FObj (Yoneda A (obj (preinitialObj PI))) b)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 621
diff changeset
280 -- tmap1 b x = arrow ( SFSFMap← SFS ( preinitialArrow PI ) )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 621
diff changeset
281 -- 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: 621
diff changeset
282 -- tmap2 b x = ( FMap U x ) ( hom ( preinitialObj PI ) ax )