Mercurial > hg > Members > kono > Proof > category
annotate freyd2.agda @ 499:511fd37d90ec
prove only limit preserving on co yoneda functor's obj
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Wed, 15 Mar 2017 12:28:50 +0900 |
parents | c981a2f0642f |
children | 01a0dda67a8b |
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 |
e8b85a05a6b2
add if U is iso to representable functor then preserve limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
3 open import Category.Sets |
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 |
e8b85a05a6b2
add if U is iso to representable functor then preserve limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
20 -- A is Locally small |
e8b85a05a6b2
add if U is iso to representable functor then preserve limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
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 |
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 ---- |
e8b85a05a6b2
add if U is iso to representable functor then preserve limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
29 -- |
e8b85a05a6b2
add if U is iso to representable functor then preserve limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
30 -- 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
|
31 -- |
e8b85a05a6b2
add if U is iso to representable functor then preserve limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
32 ---- |
e8b85a05a6b2
add if U is iso to representable functor then preserve limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
33 |
e8b85a05a6b2
add if U is iso to representable functor then preserve limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
34 open NTrans |
e8b85a05a6b2
add if U is iso to representable functor then preserve limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
35 open Functor |
498
c981a2f0642f
UpreseveLimit detailing
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
497
diff
changeset
|
36 open Limit |
c981a2f0642f
UpreseveLimit detailing
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
497
diff
changeset
|
37 open IsLimit |
c981a2f0642f
UpreseveLimit detailing
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
497
diff
changeset
|
38 open import Category.Cat |
497
e8b85a05a6b2
add if U is iso to representable functor then preserve limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
39 |
e8b85a05a6b2
add if U is iso to representable functor then preserve limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
40 HomA : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) (a : Obj A) → Functor A (Sets {c₂}) |
e8b85a05a6b2
add if U is iso to representable functor then preserve limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
41 HomA {c₁} {c₂} {ℓ} A a = record { |
e8b85a05a6b2
add if U is iso to representable functor then preserve limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
42 FObj = λ b → Hom A a b |
e8b85a05a6b2
add if U is iso to representable functor then preserve limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
43 ; FMap = λ {x} {y} (f : Hom A x y ) → λ ( g : Hom A a x ) → A [ f o g ] -- f : Hom A x y → Hom Sets (Hom A a x ) (Hom A a y) |
e8b85a05a6b2
add if U is iso to representable functor then preserve limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
44 ; isFunctor = record { |
e8b85a05a6b2
add if U is iso to representable functor then preserve limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
45 identity = λ {b} → extensionality A ( λ x → lemma-y-obj1 {b} x ) ; |
e8b85a05a6b2
add if U is iso to representable functor then preserve limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
46 distr = λ {a} {b} {c} {f} {g} → extensionality A ( λ x → lemma-y-obj2 a b c f g x ) ; |
e8b85a05a6b2
add if U is iso to representable functor then preserve limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
47 ≈-cong = λ eq → extensionality A ( λ x → lemma-y-obj3 x eq ) |
e8b85a05a6b2
add if U is iso to representable functor then preserve limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
48 } |
e8b85a05a6b2
add if U is iso to representable functor then preserve limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
49 } where |
e8b85a05a6b2
add if U is iso to representable functor then preserve limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
50 lemma-y-obj1 : {b : Obj A } → (x : Hom A a b) → A [ id1 A b o x ] ≡ x |
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-obj1 {b} x = let open ≈-Reasoning A in ≈-≡ {_} {_} {_} {A} idL |
e8b85a05a6b2
add if U is iso to representable functor then preserve limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
52 lemma-y-obj2 : (a₁ b c : Obj A) (f : Hom A a₁ b) (g : Hom A b c ) → (x : Hom A a a₁ )→ |
e8b85a05a6b2
add if U is iso to representable functor then preserve limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
53 A [ A [ g o f ] o x ] ≡ (Sets [ _[_o_] A g o _[_o_] A f ]) x |
e8b85a05a6b2
add if U is iso to representable functor then preserve limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
54 lemma-y-obj2 a₁ b c f g x = let open ≈-Reasoning A in ≈-≡ {_} {_} {_} {A} ( begin |
e8b85a05a6b2
add if U is iso to representable functor then preserve limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
55 A [ A [ g o f ] o x ] |
e8b85a05a6b2
add if U is iso to representable functor then preserve limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
56 ≈↑⟨ assoc ⟩ |
e8b85a05a6b2
add if U is iso to representable functor then preserve limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
57 A [ g o A [ f o x ] ] |
e8b85a05a6b2
add if U is iso to representable functor then preserve limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
58 ≈⟨⟩ |
e8b85a05a6b2
add if U is iso to representable functor then preserve limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
59 ( λ x → A [ g o x ] ) ( ( λ x → A [ f o x ] ) x ) |
e8b85a05a6b2
add if U is iso to representable functor then preserve limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
60 ∎ ) |
e8b85a05a6b2
add if U is iso to representable functor then preserve limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
61 lemma-y-obj3 : {b c : Obj A} {f g : Hom A b c } → (x : Hom A a b ) → A [ f ≈ g ] → A [ f o x ] ≡ A [ g o x ] |
e8b85a05a6b2
add if U is iso to representable functor then preserve limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
62 lemma-y-obj3 {_} {_} {f} {g} x eq = let open ≈-Reasoning A in ≈-≡ {_} {_} {_} {A} ( begin |
e8b85a05a6b2
add if U is iso to representable functor then preserve limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
63 A [ f o x ] |
e8b85a05a6b2
add if U is iso to representable functor then preserve limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
64 ≈⟨ resp refl-hom eq ⟩ |
e8b85a05a6b2
add if U is iso to representable functor then preserve limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
65 A [ g o x ] |
e8b85a05a6b2
add if U is iso to representable functor then preserve limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
66 ∎ ) |
e8b85a05a6b2
add if U is iso to representable functor then preserve limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
67 |
e8b85a05a6b2
add if U is iso to representable functor then preserve limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
68 |
499
511fd37d90ec
prove only limit preserving on co yoneda functor's obj
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
498
diff
changeset
|
69 HpreseveLimit : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) → (b : Obj A) |
497
e8b85a05a6b2
add if U is iso to representable functor then preserve limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
70 { c₁' c₂' ℓ' : Level} ( I : Category c₁' c₂' ℓ' ) |
499
511fd37d90ec
prove only limit preserving on co yoneda functor's obj
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
498
diff
changeset
|
71 → LimitPreserve A I (Sets {c₂}) ( HomA A b ) |
511fd37d90ec
prove only limit preserving on co yoneda functor's obj
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
498
diff
changeset
|
72 HpreseveLimit {_} { c₂} A b I = record { |
498
c981a2f0642f
UpreseveLimit detailing
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
497
diff
changeset
|
73 preserve = λ Γ limita → record { |
c981a2f0642f
UpreseveLimit detailing
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
497
diff
changeset
|
74 limit = λ a t → limitu a Γ t limita |
c981a2f0642f
UpreseveLimit detailing
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
497
diff
changeset
|
75 ; t0f=t = λ { a t i } → t0f=tu {a} Γ t limita {i} |
c981a2f0642f
UpreseveLimit detailing
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
497
diff
changeset
|
76 ; limit-uniqueness = λ { a t f } t=f → limit-uniquenessu {a} Γ limita t f t=f |
c981a2f0642f
UpreseveLimit detailing
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
497
diff
changeset
|
77 } |
c981a2f0642f
UpreseveLimit detailing
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
497
diff
changeset
|
78 } where |
499
511fd37d90ec
prove only limit preserving on co yoneda functor's obj
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
498
diff
changeset
|
79 limitu : ( a : Obj Sets ) → (Γ : Functor I A ) ( t : NTrans I Sets ( K Sets I a ) ((HomA A b) ○ Γ) ) → ( limita : Limit A I Γ ) → |
511fd37d90ec
prove only limit preserving on co yoneda functor's obj
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
498
diff
changeset
|
80 Hom Sets a (FObj (HomA A b) (a0 limita)) |
498
c981a2f0642f
UpreseveLimit detailing
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
497
diff
changeset
|
81 limitu = {!!} |
499
511fd37d90ec
prove only limit preserving on co yoneda functor's obj
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
498
diff
changeset
|
82 t0f=tu : { a : Obj Sets } → (Γ : Functor I A ) ( t : NTrans I Sets ( K Sets I a ) ((HomA A b) ○ Γ) ) → ( limita : Limit A I Γ ) → |
511fd37d90ec
prove only limit preserving on co yoneda functor's obj
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
498
diff
changeset
|
83 ∀ { i : Obj I } → Sets [ Sets [ TMap (LimitNat A I Sets Γ (a0 limita) (t0 limita) (HomA A b)) i o limitu a Γ t limita ] ≈ TMap t i ] |
498
c981a2f0642f
UpreseveLimit detailing
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
497
diff
changeset
|
84 t0f=tu = {!!} |
499
511fd37d90ec
prove only limit preserving on co yoneda functor's obj
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
498
diff
changeset
|
85 limit-uniquenessu : { a : Obj Sets } → (Γ : Functor I A ) |
498
c981a2f0642f
UpreseveLimit detailing
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
497
diff
changeset
|
86 → ( limita : Limit A I Γ ) → |
499
511fd37d90ec
prove only limit preserving on co yoneda functor's obj
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
498
diff
changeset
|
87 ( t : NTrans I Sets ( K Sets I a ) ((HomA A b) ○ Γ) ) → ( f : Hom Sets a (FObj (HomA A b) (a0 limita)) ) |
511fd37d90ec
prove only limit preserving on co yoneda functor's obj
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
498
diff
changeset
|
88 → ( ∀ { i : Obj I } → (Sets [ TMap (LimitNat A I Sets Γ (a0 limita) (t0 limita) (HomA A b)) i o f ] ≡ TMap t i ) ) |
498
c981a2f0642f
UpreseveLimit detailing
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
497
diff
changeset
|
89 → Sets [ limitu a Γ t limita ≈ f ] |
c981a2f0642f
UpreseveLimit detailing
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
497
diff
changeset
|
90 limit-uniquenessu = {!!} |
c981a2f0642f
UpreseveLimit detailing
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
497
diff
changeset
|
91 |
499
511fd37d90ec
prove only limit preserving on co yoneda functor's obj
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
498
diff
changeset
|
92 |
511fd37d90ec
prove only limit preserving on co yoneda functor's obj
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
498
diff
changeset
|
93 |
511fd37d90ec
prove only limit preserving on co yoneda functor's obj
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
498
diff
changeset
|
94 -- record Representable { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) ( U : Functor A (Sets {c₂}) ) (b : Obj A) : Set (suc ℓ ⊔ (suc (suc c₂) ⊔ suc c₁ )) where |
511fd37d90ec
prove only limit preserving on co yoneda functor's obj
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
498
diff
changeset
|
95 -- field |
511fd37d90ec
prove only limit preserving on co yoneda functor's obj
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
498
diff
changeset
|
96 -- -- FObj U x : A → Set |
511fd37d90ec
prove only limit preserving on co yoneda functor's obj
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
498
diff
changeset
|
97 -- -- FMap U f = Set → Set |
511fd37d90ec
prove only limit preserving on co yoneda functor's obj
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
498
diff
changeset
|
98 -- -- λ b → Hom (a,b) : A → Set |
511fd37d90ec
prove only limit preserving on co yoneda functor's obj
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
498
diff
changeset
|
99 -- -- λ f → Hom (a,-) = λ b → Hom a b |
511fd37d90ec
prove only limit preserving on co yoneda functor's obj
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
498
diff
changeset
|
100 -- |
511fd37d90ec
prove only limit preserving on co yoneda functor's obj
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
498
diff
changeset
|
101 -- repr→ : NTrans A (Sets {c₂}) U (HomA A b ) |
511fd37d90ec
prove only limit preserving on co yoneda functor's obj
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
498
diff
changeset
|
102 -- repr← : NTrans A (Sets {c₂}) (HomA A b) U |
511fd37d90ec
prove only limit preserving on co yoneda functor's obj
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
498
diff
changeset
|
103 -- representable→ : {x : Obj A} → Sets [ Sets [ TMap repr→ x o TMap repr← x ] ≈ id1 (Sets {c₂}) (FObj (HomA A b) x )] |
511fd37d90ec
prove only limit preserving on co yoneda functor's obj
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
498
diff
changeset
|
104 -- representable← : {x : Obj A} → Sets [ Sets [ TMap repr← x o TMap repr→ x ] ≈ id1 (Sets {c₂}) (FObj U x)] |
511fd37d90ec
prove only limit preserving on co yoneda functor's obj
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
498
diff
changeset
|
105 -- |
511fd37d90ec
prove only limit preserving on co yoneda functor's obj
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
498
diff
changeset
|
106 -- |
511fd37d90ec
prove only limit preserving on co yoneda functor's obj
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
498
diff
changeset
|
107 -- UpreseveLimit : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) → ( U : Functor A (Sets {c₂}) ) (b : Obj A) |
511fd37d90ec
prove only limit preserving on co yoneda functor's obj
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
498
diff
changeset
|
108 -- { c₁' c₂' ℓ' : Level} ( I : Category c₁' c₂' ℓ' ) |
511fd37d90ec
prove only limit preserving on co yoneda functor's obj
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
498
diff
changeset
|
109 -- ( rep : Representable A U b ) → LimitPreserve A I (Sets {c₂}) U |
511fd37d90ec
prove only limit preserving on co yoneda functor's obj
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
498
diff
changeset
|
110 -- UpreseveLimit {_} { c₂} A U b I rep = record { |
511fd37d90ec
prove only limit preserving on co yoneda functor's obj
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
498
diff
changeset
|
111 -- preserve = λ Γ limita → record { |
511fd37d90ec
prove only limit preserving on co yoneda functor's obj
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
498
diff
changeset
|
112 -- limit = λ a t → limitu a Γ t limita |
511fd37d90ec
prove only limit preserving on co yoneda functor's obj
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
498
diff
changeset
|
113 -- ; t0f=t = λ { a t i } → t0f=tu {a} Γ t limita {i} |
511fd37d90ec
prove only limit preserving on co yoneda functor's obj
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
498
diff
changeset
|
114 -- ; limit-uniqueness = λ { a t f } t=f → limit-uniquenessu {a} Γ limita t f t=f |
511fd37d90ec
prove only limit preserving on co yoneda functor's obj
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
498
diff
changeset
|
115 -- } |
511fd37d90ec
prove only limit preserving on co yoneda functor's obj
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
498
diff
changeset
|
116 -- } where |
511fd37d90ec
prove only limit preserving on co yoneda functor's obj
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
498
diff
changeset
|
117 -- limitu : ( a : Obj (Sets {c₂}) ) → (Γ : Functor I A ) ( t : NTrans I Sets ( K Sets I a ) (U ○ Γ) ) → ( limita : Limit A I Γ ) → |
511fd37d90ec
prove only limit preserving on co yoneda functor's obj
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
498
diff
changeset
|
118 -- Hom Sets a (FObj U (a0 limita)) |
511fd37d90ec
prove only limit preserving on co yoneda functor's obj
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
498
diff
changeset
|
119 -- limitu = {!!} |
511fd37d90ec
prove only limit preserving on co yoneda functor's obj
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
498
diff
changeset
|
120 -- t0f=tu : { a : Obj (Sets {c₂}) } → (Γ : Functor I A ) ( t : NTrans I Sets ( K Sets I a ) (U ○ Γ) ) → ( limita : Limit A I Γ ) → |
511fd37d90ec
prove only limit preserving on co yoneda functor's obj
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
498
diff
changeset
|
121 -- ∀ { i : Obj I } → Sets [ Sets [ TMap (LimitNat A I Sets Γ (a0 limita) (t0 limita) U) i o limitu a Γ t limita ] ≈ TMap t i ] |
511fd37d90ec
prove only limit preserving on co yoneda functor's obj
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
498
diff
changeset
|
122 -- t0f=tu = {!!} |
511fd37d90ec
prove only limit preserving on co yoneda functor's obj
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
498
diff
changeset
|
123 -- limit-uniquenessu : { a : Obj (Sets {c₂}) } → (Γ : Functor I A ) |
511fd37d90ec
prove only limit preserving on co yoneda functor's obj
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
498
diff
changeset
|
124 -- → ( limita : Limit A I Γ ) → |
511fd37d90ec
prove only limit preserving on co yoneda functor's obj
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
498
diff
changeset
|
125 -- ( t : NTrans I Sets ( K Sets I a ) (U ○ Γ) ) → ( f : Hom Sets a (FObj U (a0 limita)) ) |
511fd37d90ec
prove only limit preserving on co yoneda functor's obj
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
498
diff
changeset
|
126 -- → ( ∀ { i : Obj I } → (Sets [ TMap (LimitNat A I Sets Γ (a0 limita) (t0 limita) U) i o f ] ≡ TMap t i ) ) |
511fd37d90ec
prove only limit preserving on co yoneda functor's obj
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
498
diff
changeset
|
127 -- → Sets [ limitu a Γ t limita ≈ f ] |
511fd37d90ec
prove only limit preserving on co yoneda functor's obj
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
498
diff
changeset
|
128 -- limit-uniquenessu = {!!} |
511fd37d90ec
prove only limit preserving on co yoneda functor's obj
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
498
diff
changeset
|
129 -- |