Mercurial > hg > Members > kono > Proof > category

comparison freyd2.agda @ 609:d686d7ae38e0

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
on goging
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 12 Jun 2017 16:35:34 +0900
parents 7194ba55df56
children 3fb4d834c349
comparison
equal deleted inserted replaced
608:7194ba55df56 609:d686d7ae38e0
15 -- a : Obj A 15 -- a : Obj A
16 -- U : A → Sets 16 -- U : A → Sets
17 -- U ⋍ Hom (a,-) 17 -- U ⋍ Hom (a,-)
18 -- 18 --
19 19
20 -- A is Locally small
21
22 ---- 20 ----
23 -- C is locally small i.e. Hom C i j is a set c₁ 21 -- C is locally small i.e. Hom C i j is a set c₁
24 -- 22 --
25 record Small { c₁ c₂ ℓ : Level} ( C : Category c₁ c₂ ℓ ) ( I : Set c₁ ) 23 record Small { c₁ c₂ ℓ : Level} ( C : Category c₁ c₂ ℓ ) ( I : Set c₁ )
26 : Set (suc (c₁ ⊔ c₂ ⊔ ℓ )) where 24 : Set (suc (c₁ ⊔ c₂ ⊔ ℓ )) where
28 hom→ : {i j : Obj C } → Hom C i j → I 26 hom→ : {i j : Obj C } → Hom C i j → I
29 hom← : {i j : Obj C } → ( f : I ) → Hom C i j 27 hom← : {i j : Obj C } → ( f : I ) → Hom C i j
30 hom-iso : {i j : Obj C } → { f : Hom C i j } → hom← ( hom→ f ) ≡ f 28 hom-iso : {i j : Obj C } → { f : Hom C i j } → hom← ( hom→ f ) ≡ f
31 29
32 open Small 30 open Small
33
34 31
35 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 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
36 33
37 import Relation.Binary.PropositionalEquality 34 import Relation.Binary.PropositionalEquality
38 -- 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 ) 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 )
77 A [ f o x ] 74 A [ f o x ]
78 ≈⟨ resp refl-hom eq ⟩ 75 ≈⟨ resp refl-hom eq ⟩
79 A [ g o x ] 76 A [ g o x ]
80 ∎ ) 77 ∎ )
81 78
79 -- Representable U ≈　Hom(A,-)
82 80
83 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
84 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
85 field 82 field
86 -- FObj U x : A → Set 83 -- FObj U x : A → Set
87 -- FMap U f = Set → Set 84 -- FMap U f = Set → Set (locally small)
88 -- λ b → Hom (a,b) : A → Set 85 -- λ b → Hom (a,b) : A → Set
89 -- λ f → Hom (a,-) = λ b → Hom a b 86 -- λ f → Hom (a,-) = λ b → Hom a b
90 87
91 repr→ : NTrans A (Sets {c₂}) U (HomA A b ) 88 repr→ : NTrans A (Sets {c₂}) U (HomA A a )
92 repr← : NTrans A (Sets {c₂}) (HomA A b) U 89 repr← : NTrans A (Sets {c₂}) (HomA A a) U
93 reprId : {x : Obj A} → Sets [ Sets [ TMap repr→ x o TMap repr← x ] ≈ id1 (Sets {c₂}) (FObj (HomA A b) x )] 90 reprId→ : {x : Obj A} → Sets [ Sets [ TMap repr→ x o TMap repr← x ] ≈ id1 (Sets {c₂}) (FObj (HomA A a) x )]
94 reprId : {x : Obj A} → Sets [ Sets [ TMap repr← x o TMap repr→ x ] ≈ id1 (Sets {c₂}) (FObj U x)] 91 reprId← : {x : Obj A} → Sets [ Sets [ TMap repr← x o TMap repr→ x ] ≈ id1 (Sets {c₂}) (FObj U x)]
95 92
93 open Representable
96 open import freyd 94 open import freyd
97 95
98 _↓_ : { c₁ c₂ ℓ : Level} { c₁' c₂' ℓ' : Level} { A : Category c₁ c₂ ℓ } { B : Category c₁' c₂' ℓ' } 96 _↓_ : { c₁ c₂ ℓ : Level} { c₁' c₂' ℓ' : Level} { A : Category c₁ c₂ ℓ } { B : Category c₁' c₂' ℓ' }
99 → ( F G : Functor A B ) 97 → ( F G : Functor A B )
100 → Category (c₂' ⊔ c₁) (ℓ' ⊔ c₂) ℓ 98 → Category (c₂' ⊔ c₁) (ℓ' ⊔ c₂) ℓ
101 _↓_ { c₁} {c₂} {ℓ} {c₁'} {c₂'} {ℓ'} { A } { B } F G = CommaCategory 99 _↓_ { c₁} {c₂} {ℓ} {c₁'} {c₂'} {ℓ'} { A } { B } F G = CommaCategory
102 where open import Comma1 F G 100 where open import Comma1 F G
103 101
104
105 open import freyd 102 open import freyd
106
107 -- K{*}↓U has preinitial full subcategory then U is representable
108
109 open SmallFullSubcategory 103 open SmallFullSubcategory
110 open Complete 104 open Complete
111 open PreInitial 105 open PreInitial
106 open HasInitialObject
107 open import Comma1
108 open CommaObj
109 open LimitPreserve
112 110
113 data OneObject : Set where 111 -- Representable Functor U preserve limit , so K{*}↓U is complete
114 * : OneObject 112
113 UpreserveLimit : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (I : Category c₁ c₂ ℓ)
114 (comp : Complete A A)
115 (U : Functor A (Sets) )
116 (a : Obj A )
117 (R : Representable A U a ) → LimitPreserve A I Sets U
118 UpreserveLimit A I comp U a R = record {
119 preserve = λ Γ lim → record {
120 limit = λ a t → {!!}
121 ; t0f=t = λ {a t i} → ?
122 ; limit-uniqueness = λ {a} {t} {f} t0f=t → {!!}
123 }
124 }
125
126 -- K{*}↓U has preinitial full subcategory then U is representable
127 -- K{*}↓U is complete, so it has initial object
115 128
116 UisRepresentable : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) 129 UisRepresentable : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ)
117 (comp : Complete A A) 130 (comp : Complete A A)
118 (U : Functor A (Sets) ) 131 (U : Functor A (Sets {c₂}) )
119 (SFS : SmallFullSubcategory ( K (Sets) {!!} {!!} ↓ U )) → 132 (a : Obj Sets )
120 (PI : PreInitial {!!} (SFSF SFS )) → Representable A U {!!} 133 (x : Obj ( K (Sets) A a ↓ U) )
121 UisRepresentable = {!!} 134 ( init : HasInitialObject {c₁} {c₂} {ℓ} ( K (Sets) A a ↓ U ) x )
135 → Representable A U (obj x)
136 UisRepresentable A comp U a x init = record {
137 repr→ = record { TMap = {!!} ; isNTrans = record { commute = {!!} } }
138 ; repr← = record { TMap = {!!} ; isNTrans = record { commute = {!!} } }
139 ; reprId→ = λ {y} →　?
140 ; reprId← = λ {y} →　?
141 }
122 142
123 -- K{*}↓U has preinitial full subcategory if U is representable 143 -- K{*}↓U has preinitial full subcategory if U is representable
144 -- if U is representable, K{*}↓U has initial Object ( so it has preinitial full subcategory )
124 145
125 KUhasSFS : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) 146 KUhasInitialObj : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ)
126 (comp : Complete A A) 147 (comp : Complete A A)
127 (U : Functor A (Sets) ) 148 (U : Functor A (Sets) )
128 (a : Obj A ) 149 (a : Obj A )
129 (R : Representable A U a ) → 150 (R : Representable A U a ) →
130 SmallFullSubcategory {!!} 151 HasInitialObject {c₁} {c₂} {ℓ} ( K (Sets) A (FObj U a) ↓ U ) ( record { obj = a ; hom = id1 Sets (FObj U a) } )
131 KUhasSFS = {!!} 152 KUhasInitialObj A comp U a R = record {
153 initial = λ b → {!!}
154 ; uniqueness = λ b f → {!!}
155 }
132 156
133 KUhasPreinitial : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ)
134 (comp : Complete A A)
135 (U : Functor A (Sets) )
136 (a : Obj A )
137 (R : Representable A U a ) →
138 PreInitial {!!} (SFSF (KUhasSFS A comp U a R ) )
139 KUhasPreinitial = {!!}