Mercurial > hg > Members > kono > Proof > category

annotate freyd2.agda @ 613:afddfebea797

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
t0f=t0 done
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Tue, 13 Jun 2017 22:36:54 +0900
parents f924056bf08a
children e6be03d94284
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
608
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 502
diff changeset
20 ----
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 502
diff changeset
21 -- C is locally small i.e. Hom C i j is a set c₁
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 502
diff changeset
22 --
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 502
diff changeset
23 record Small { c₁ c₂ ℓ : Level} ( C : Category c₁ c₂ ℓ ) ( I : Set c₁ )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 502
diff changeset
24 : Set (suc (c₁ ⊔ c₂ ⊔ ℓ )) where
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 502
diff changeset
25 field
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 502
diff changeset
26 hom→ : {i j : Obj C } → Hom C i j → I
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 502
diff changeset
27 hom← : {i j : Obj C } → ( f : I ) → Hom C i j
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 502
diff changeset
28 hom-iso : {i j : Obj C } → { f : Hom C i j } → hom← ( hom→ f ) ≡ f
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 502
diff changeset
29
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 502
diff changeset
30 open Small
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 502
diff changeset
31
611
b1b5c6b4c570 natural transformation in representable functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 610
diff changeset
32 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
33
e8b85a05a6b2 add if U is iso to representable functor then preserve limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
34 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
35 -- 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
36 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
37
e8b85a05a6b2 add if U is iso to representable functor then preserve limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
38
e8b85a05a6b2 add if U is iso to representable functor then preserve limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
39 ----
e8b85a05a6b2 add if U is iso to representable functor then preserve limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
40 --
e8b85a05a6b2 add if U is iso to representable functor then preserve limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
41 -- Hom ( a, - ) is Object mapping in co Yoneda Functor
e8b85a05a6b2 add if U is iso to representable functor then preserve limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
42 --
e8b85a05a6b2 add if U is iso to representable functor then preserve limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
43 ----
e8b85a05a6b2 add if U is iso to representable functor then preserve limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
44
e8b85a05a6b2 add if U is iso to representable functor then preserve limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
45 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
46 open Functor
498
c981a2f0642f UpreseveLimit detailing
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 497
diff changeset
47 open Limit
c981a2f0642f UpreseveLimit detailing
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 497
diff changeset
48 open IsLimit
c981a2f0642f UpreseveLimit detailing
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 497
diff changeset
49 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
50
e8b85a05a6b2 add if U is iso to representable functor then preserve limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
51 HomA : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) (a : Obj A) → Functor A (Sets {c₂})
611
b1b5c6b4c570 natural transformation in representable functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 610
diff changeset
52 HomA {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
53 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
54 ; 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
55 ; 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
56 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
57 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
58 ≈-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
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 } where
e8b85a05a6b2 add if U is iso to representable functor then preserve limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
61 lemma-y-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
62 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
63 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
64 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
65 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
66 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
67 ≈↑⟨ assoc ⟩
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 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
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 ( λ 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
71 ∎ )
e8b85a05a6b2 add if U is iso to representable functor then preserve limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
72 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
73 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
74 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
75 ≈⟨ 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
76 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
77 ∎ )
e8b85a05a6b2 add if U is iso to representable functor then preserve limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
78
609
d686d7ae38e0 on goging
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 608
diff changeset
79 -- Representable U ≈　Hom(A,-)
502
01a0dda67a8b on going ..
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 499
diff changeset
80
609
d686d7ae38e0 on goging
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 608
diff changeset
81 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
82 field
01a0dda67a8b on going ..
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 499
diff changeset
83 -- FObj U x : A → Set
609
d686d7ae38e0 on goging
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 608
diff changeset
84 -- FMap U f = Set → Set (locally small)
502
01a0dda67a8b on going ..
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 499
diff changeset
85 -- λ b → Hom (a,b) : A → Set
01a0dda67a8b on going ..
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 499
diff changeset
86 -- λ f → Hom (a,-) = λ b → Hom a b
01a0dda67a8b on going ..
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 499
diff changeset
87
609
d686d7ae38e0 on goging
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 608
diff changeset
88 repr→ : NTrans A (Sets {c₂}) U (HomA A a )
d686d7ae38e0 on goging
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 608
diff changeset
89 repr← : NTrans A (Sets {c₂}) (HomA A a) U
d686d7ae38e0 on goging
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 608
diff changeset
90 reprId→ : {x : Obj A} → Sets [ Sets [ TMap repr→ x o TMap repr← x ] ≈ id1 (Sets {c₂}) (FObj (HomA A a) x )]
d686d7ae38e0 on goging
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 608
diff changeset
91 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
92
609
d686d7ae38e0 on goging
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 608
diff changeset
93 open Representable
608
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 502
diff changeset
94 open import freyd
502
01a0dda67a8b on going ..
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 499
diff changeset
95
608
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 502
diff changeset
96 _↓_ : { c₁ c₂ ℓ : Level} { c₁' c₂' ℓ' : Level} { A : Category c₁ c₂ ℓ } { B : Category c₁' c₂' ℓ' }
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 502
diff changeset
97 → ( F G : Functor A B )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 502
diff changeset
98 → Category (c₂' ⊔ c₁) (ℓ' ⊔ c₂) ℓ
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 502
diff changeset
99 _↓_ { c₁} {c₂} {ℓ} {c₁'} {c₂'} {ℓ'} { A } { B } F G = CommaCategory
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 502
diff changeset
100 where open import Comma1 F G
498
c981a2f0642f UpreseveLimit detailing
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 497
diff changeset
101
608
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 502
diff changeset
102 open import freyd
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 502
diff changeset
103 open SmallFullSubcategory
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 502
diff changeset
104 open Complete
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 502
diff changeset
105 open PreInitial
609
d686d7ae38e0 on goging
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 608
diff changeset
106 open HasInitialObject
d686d7ae38e0 on goging
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 608
diff changeset
107 open import Comma1
d686d7ae38e0 on goging
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 608
diff changeset
108 open CommaObj
d686d7ae38e0 on goging
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 608
diff changeset
109 open LimitPreserve
608
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 502
diff changeset
110
609
d686d7ae38e0 on goging
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 608
diff changeset
111 -- 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
112 --
3fb4d834c349 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 609
diff changeset
113 -- HomA A b = λ a → Hom A a b : Functor A Sets
3fb4d834c349 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 609
diff changeset
114 -- : Functor Sets A
3fb4d834c349 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 609
diff changeset
115
3fb4d834c349 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 609
diff changeset
116 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
117 (b : Obj A )
610
3fb4d834c349 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 609
diff changeset
118 (Γ : Functor I A) (limita : Limit A I Γ) →
3fb4d834c349 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 609
diff changeset
119 IsLimit Sets I (HomA A b ○ Γ) (FObj (HomA A b) (a0 limita)) (LimitNat A I Sets Γ (a0 limita) (t0 limita) (HomA A b))
612
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 611
diff changeset
120 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
121 limit = λ a t → ψ a t
b1b5c6b4c570 natural transformation in representable functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 610
diff changeset
122 ; t0f=t = λ {a t i} → t0f=t0 a t i
610
3fb4d834c349 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 609
diff changeset
123 ; limit-uniqueness = λ {b} {t} {f} t0f=t → {!!}
3fb4d834c349 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 609
diff changeset
124 } where
611
b1b5c6b4c570 natural transformation in representable functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 610
diff changeset
125 hat0 : NTrans I Sets (K Sets I (FObj (HomA A b) (a0 lim))) (HomA A b ○ Γ)
b1b5c6b4c570 natural transformation in representable functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 610
diff changeset
126 hat0 = LimitNat A I Sets Γ (a0 lim) (t0 lim) (HomA A b)
b1b5c6b4c570 natural transformation in representable functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 610
diff changeset
127 haa0 : Obj Sets
b1b5c6b4c570 natural transformation in representable functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 610
diff changeset
128 haa0 = FObj (HomA A b) (a0 lim)
b1b5c6b4c570 natural transformation in representable functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 610
diff changeset
129 ta : (a : Obj Sets) ( x : a ) ( t : NTrans I Sets (K Sets I a) (HomA A b ○ Γ)) → NTrans I A (K A I b ) Γ
b1b5c6b4c570 natural transformation in representable functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 610
diff changeset
130 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
131 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
132 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
133 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
134 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
135 ≈⟨⟩
b1b5c6b4c570 natural transformation in representable functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 610
diff changeset
136 ( ( FMap (HomA A b ○ Γ ) f ) * TMap t a₁ ) x
b1b5c6b4c570 natural transformation in representable functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 610
diff changeset
137 ≈⟨ ≡-≈ ( 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
138 ( 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
139 ≈⟨⟩
b1b5c6b4c570 natural transformation in representable functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 610
diff changeset
140 ( 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
141 ≈⟨⟩
b1b5c6b4c570 natural transformation in representable functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 610
diff changeset
142 TMap t b₁ x
b1b5c6b4c570 natural transformation in representable functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 610
diff changeset
143 ≈↑⟨ idR ⟩
b1b5c6b4c570 natural transformation in representable functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 610
diff changeset
144 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
145 ≈⟨⟩
b1b5c6b4c570 natural transformation in representable functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 610
diff changeset
146 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
147 ∎
b1b5c6b4c570 natural transformation in representable functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 610
diff changeset
148 ψ : (X : Obj Sets) ( t : NTrans I Sets (K Sets I X) (HomA A b ○ Γ))
b1b5c6b4c570 natural transformation in representable functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 610
diff changeset
149 → Hom Sets X (FObj (HomA A b) (a0 lim))
b1b5c6b4c570 natural transformation in representable functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 610
diff changeset
150 ψ X t x = FMap (HomA A b) (limit (isLimit lim) b (ta X x t )) (id1 A b )
b1b5c6b4c570 natural transformation in representable functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 610
diff changeset
151 t0f=t0 : (a : Obj Sets ) ( t : NTrans I Sets (K Sets I a) (HomA A b ○ Γ)) (i : Obj I)
b1b5c6b4c570 natural transformation in representable functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 610
diff changeset
152 → Sets [ Sets [ TMap (LimitNat A I Sets Γ (a0 lim) (t0 lim) (HomA A b)) i o ψ a t ] ≈ TMap t i ]
612
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 611
diff changeset
153 t0f=t0 a t i = let open ≈-Reasoning A in extensionality A ( λ x → ≈-≡ A ( begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 611
diff changeset
154 ( Sets [ TMap (LimitNat A I Sets Γ (a0 lim) (t0 lim) (HomA A b)) i o ψ a t ] ) x
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 611
diff changeset
155 ≈⟨⟩
613
afddfebea797 t0f=t0 done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 612
diff changeset
156 FMap (HomA A b) ( TMap (t0 lim) i) (FMap (HomA A b) (limit (isLimit lim) b (ta a x t )) (id1 A b ))
afddfebea797 t0f=t0 done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 612
diff changeset
157 ≈⟨⟩
afddfebea797 t0f=t0 done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 612
diff changeset
158 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
159 ≈⟨ cdr idR ⟩
afddfebea797 t0f=t0 done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 612
diff changeset
160 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
161 ≈⟨ t0f=t (isLimit lim) ⟩
afddfebea797 t0f=t0 done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 612
diff changeset
162 TMap (ta a x t) i
afddfebea797 t0f=t0 done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 612
diff changeset
163 ≈⟨⟩
612
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 611
diff changeset
164 TMap t i x
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 611
diff changeset
165 ∎ ))
610
3fb4d834c349 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 609
diff changeset
166
609
d686d7ae38e0 on goging
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 608
diff changeset
167
d686d7ae38e0 on goging
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 608
diff changeset
168 UpreserveLimit : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (I : Category c₁ c₂ ℓ)
612
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 611
diff changeset
169 (b : Obj A ) → LimitPreserve A I Sets (HomA A b)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 611
diff changeset
170 UpreserveLimit A I b = record {
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 611
diff changeset
171 preserve = λ Γ lim → UpreserveLimit0 A I b Γ lim
610
3fb4d834c349 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 609
diff changeset
172 }
609
d686d7ae38e0 on goging
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 608
diff changeset
173
d686d7ae38e0 on goging
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 608
diff changeset
174 -- K{*}↓U has preinitial full subcategory then U is representable
d686d7ae38e0 on goging
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 608
diff changeset
175 -- K{*}↓U is complete, so it has initial object
608
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 502
diff changeset
176
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 502
diff changeset
177 UisRepresentable : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 502
diff changeset
178 (comp : Complete A A)
609
d686d7ae38e0 on goging
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 608
diff changeset
179 (U : Functor A (Sets {c₂}) )
d686d7ae38e0 on goging
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 608
diff changeset
180 (a : Obj Sets )
d686d7ae38e0 on goging
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 608
diff changeset
181 (x : Obj ( K (Sets) A a ↓ U) )
d686d7ae38e0 on goging
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 608
diff changeset
182 ( init : HasInitialObject {c₁} {c₂} {ℓ} ( K (Sets) A a ↓ U ) x )
d686d7ae38e0 on goging
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 608
diff changeset
183 → Representable A U (obj x)
d686d7ae38e0 on goging
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 608
diff changeset
184 UisRepresentable A comp U a x init = record {
d686d7ae38e0 on goging
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 608
diff changeset
185 repr→ = record { TMap = {!!} ; isNTrans = record { commute = {!!} } }
d686d7ae38e0 on goging
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 608
diff changeset
186 ; repr← = record { TMap = {!!} ; isNTrans = record { commute = {!!} } }
d686d7ae38e0 on goging
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 608
diff changeset
187 ; reprId→ = λ {y} →　?
d686d7ae38e0 on goging
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 608
diff changeset
188 ; reprId← = λ {y} →　?
d686d7ae38e0 on goging
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 608
diff changeset
189 }
608
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 502
diff changeset
190
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 502
diff changeset
191 -- 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
192 -- 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
193
609
d686d7ae38e0 on goging
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 608
diff changeset
194 KUhasInitialObj : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ)
608
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 502
diff changeset
195 (comp : Complete A A)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 502
diff changeset
196 (U : Functor A (Sets) )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 502
diff changeset
197 (a : Obj A )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 502
diff changeset
198 (R : Representable A U a ) →
609
d686d7ae38e0 on goging
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 608
diff changeset
199 HasInitialObject {c₁} {c₂} {ℓ} ( K (Sets) A (FObj U a) ↓ U ) ( record { obj = a ; hom = id1 Sets (FObj U a) } )
d686d7ae38e0 on goging
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 608
diff changeset
200 KUhasInitialObj A comp U a R = record {
d686d7ae38e0 on goging
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 608
diff changeset
201 initial = λ b → {!!}
d686d7ae38e0 on goging
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 608
diff changeset
202 ; uniqueness = λ b f → {!!}
d686d7ae38e0 on goging
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 608
diff changeset
203 }
608
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 502
diff changeset
204