Mercurial > hg > Members > kono > Proof > category

comparison src/CCC.agda @ 975:f8fba4f1dcfa

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
char-m=⊤
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 01 Mar 2021 17:01:00 +0900
parents 5731ffd6cf7a
children 8ffdc897f29b
comparison
equal deleted inserted replaced
974:5731ffd6cf7a 975:f8fba4f1dcfa
161 field 161 field
162 isMono : {c : Obj A} ( f g : Hom A c b ) → A [ A [ mono o f ] ≈ A [ mono o g ] ] → A [ f ≈ g ] 162 isMono : {c : Obj A} ( f g : Hom A c b ) → A [ A [ mono o f ] ≈ A [ mono o g ] ] → A [ f ≈ g ]
163 163
164 open Mono 164 open Mono
165 165
166 record IsTopos {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) ( １ : Obj A) (○ : (a : Obj A ) → Hom A a １) 166 record IsTopos {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (c : CCC A)
167 ( Ω : Obj A ) 167 ( Ω : Obj A )
168 ( ⊤ : Hom A １ Ω ) 168 ( ⊤ : Hom A (CCC.１ c) Ω )
169 (Ker : {a : Obj A} → ( h : Hom A a Ω ) → Equalizer A h (A [ ⊤ o (○ a) ])) 169 (Ker : {a : Obj A} → ( h : Hom A a Ω ) → Equalizer A h (A [ ⊤ o (CCC.○ c a) ]))
170 (char : {a b : Obj A} → (m : Hom A b a) → Mono A m → Hom A a Ω) : Set ( suc c₁ ⊔ suc c₂ ⊔ suc ℓ ) where 170 (char : {a b : Obj A} → (m : Hom A b a) → Mono A m → Hom A a Ω) : Set ( suc c₁ ⊔ suc c₂ ⊔ suc ℓ ) where
171 field 171 field
172 char-ker : {a b : Obj A } {h : Hom A a Ω} 172 char-ker : {a b : Obj A } {h : Hom A a Ω} (m : Hom A b a) → (mono : Mono A m)
173 → A [ char (equalizer (Ker h)) record { isMono = λ f g → monic (Ker h) } ≈ h ] 173 → A [ char m mono ≈ h ]
174 ker-char : {a b : Obj A} → (m : Hom A b a) → (mono : Mono A m) → Iso A b ( equalizer-c (Ker ( char m mono ))) 174 ker-char : {a b : Obj A} → (m : Hom A b a) → (mono : Mono A m) → Iso A b ( equalizer-c (Ker ( char m mono )))
175 175
176 record Topos {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) ( １ : Obj A) (○ : (a : Obj A ) → Hom A a １) : Set ( suc c₁ ⊔ suc c₂ ⊔ suc ℓ ) where 176 record Topos {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (c : CCC A) : Set ( suc c₁ ⊔ suc c₂ ⊔ suc ℓ ) where
177 field 177 field
178 Ω : Obj A 178 Ω : Obj A
179 ⊤ : Hom A １ Ω 179 ⊤ : Hom A (CCC.１ c) Ω
180 Ker : {a : Obj A} → ( h : Hom A a Ω ) → Equalizer A h (A [ ⊤ o (○ a) ]) 180 Ker : {a : Obj A} → ( h : Hom A a Ω ) → Equalizer A h (A [ ⊤ o (CCC.○ c a) ])
181 char : {a b : Obj A} → (m : Hom A b a ) → Mono A m → Hom A a Ω 181 char : {a b : Obj A} → (m : Hom A b a ) → Mono A m → Hom A a Ω
182 isTopos : IsTopos A １ ○ Ω ⊤ Ker char 182 isTopos : IsTopos A c Ω ⊤ Ker char
183 ker : {a : Obj A} → ( h : Hom A a Ω ) → Hom A ( equalizer-c (Ker h) ) a 183 ker : {a : Obj A} → ( h : Hom A a Ω ) → Hom A ( equalizer-c (Ker h) ) a
184 ker h = equalizer (Ker h) 184 ker h = equalizer (Ker h)
185 Monik : {a : Obj A} (h : Hom A a Ω) → Mono A (equalizer (Ker h)) 185 Monik : {a : Obj A} (h : Hom A a Ω) → Mono A (equalizer (Ker h))
186 Monik h = record { isMono = λ f g → monic (Ker h ) } 186 Monik h = record { isMono = λ f g → monic (Ker h ) }
187 char-m=⊤ : {a b : Obj A} → (m : Hom A b a) → (mono : Mono A m) → A [ A [ char m mono o m ] ≈ A [ ⊤ o CCC.○ c b ] ]
188 char-m=⊤ {a} {b} m mono = begin
189 char m mono o m ≈⟨ car (IsTopos.char-ker isTopos m mono) ⟩
190 (⊤ o CCC.○ c a) o m ≈↑⟨ assoc ⟩
191 ⊤ o (CCC.○ c a o m ) ≈⟨ cdr (IsCCC.e2 (CCC.isCCC c)) ⟩
192 ⊤ o CCC.○ c b ∎ where open ≈-Reasoning A
187 193
188 record NatD {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) ( １ : Obj A) : Set ( suc c₁ ⊔ suc c₂ ⊔ suc ℓ ) where 194 record NatD {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) ( １ : Obj A) : Set ( suc c₁ ⊔ suc c₂ ⊔ suc ℓ ) where
189 field 195 field
190 Nat : Obj A 196 Nat : Obj A
191 nzero : Hom A １ Nat 197 nzero : Hom A １ Nat