Mercurial > hg > Members > kono > Proof > category

changeset 950:bd32a37784b0 current

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Topos start
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Fri, 19 Feb 2021 09:52:31 +0900
parents ac53803b3b2a
children ae3551ded289
files CategoryExcercise.agda-lib CategoryExcercise.agda-pkg src/CCC.agda
diffstat 3 files changed, 40 insertions(+), 3 deletions(-) [+]
line wrap: on
line diff
--- a/CategoryExcercise.agda-lib	Mon Dec 21 16:40:15 2020 +0900
+++ b/CategoryExcercise.agda-lib	Fri Feb 19 09:52:31 2021 +0900
@@ -1,6 +1,6 @@
 -- File generated by Agda-Pkg
 name:    CategoryExcercise
-depend:  standard-library Category
+depend:  standard-library category-agda
 include: src
 
 -- End 
--- a/CategoryExcercise.agda-pkg	Mon Dec 21 16:40:15 2020 +0900
+++ b/CategoryExcercise.agda-pkg	Fri Feb 19 09:52:31 2021 +0900
@@ -11,7 +11,7 @@
 description:       CategoryExcercise is an Agda library ...
 depend:
     - standard-library
-    - Category
+    - category-agda
 include:
     - src
 # End 
--- a/src/CCC.agda	Mon Dec 21 16:40:15 2020 +0900
+++ b/src/CCC.agda	Fri Feb 19 09:52:31 2021 +0900
@@ -1,7 +1,8 @@
 open import Level
-open import Category 
+open import Category
 module CCC where
 
+
 open import HomReasoning
 open import cat-utility
 open  import  Relation.Binary.PropositionalEquality
@@ -121,7 +122,43 @@
          ε : {a b : Obj A } → Hom A ((a <= b ) ∧ b) a 
          isCCC : IsCCC A １ ○ _∧_ <_,_> π π' _<=_ _* ε 
 
+open Equalizer
+
+mono :  {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) {a b c : Obj A} (m : Hom A b c) → ( f g : Hom A a b ) → Set ( c₁  ⊔  c₂ ⊔ ℓ )
+mono A m f g = A [ A [ m o f ]  ≈ A [ m o g ] ] → A [ f ≈ g ]
+
+record IsTopos {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) ( １ : Obj A) (○ : (a : Obj A ) → Hom A a １)
+        (Ker : {a : Obj A} → ( h : Hom A a Ω ) → Equalizer A h (A [ ⊤ o (○ a) ]))
+        (char : {a b : Obj A} → ( m : Hom A b a ) → mono A m  → Hom A a Ω) where
+     field
+         char-ker-id  : {a : Obj A } {h : Hom A a Ω} → A [ char ( equalizer (Ker h))  ≈ h ]
+         ker-char-iso : {a b : Obj A} → ( m : Hom A b a ) → mono A m  → Iso A b (  equalizer (Ker ( char m ))) 
+
+record Topos {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) :  Set ( c₁  ⊔  c₂ ⊔ ℓ ) where
+     field
+         １ : Obj A 
+         ○ : (a : Obj A ) → Hom A a １ 
+         _∧_ : Obj A → Obj A → Obj A   
+         <_,_> : {a b c : Obj A } → Hom A c a → Hom A c b → Hom A c (a ∧ b)  
+         π : {a b : Obj A } → Hom A (a ∧ b) a 
+         π' : {a b : Obj A } → Hom A (a ∧ b) b  
+         _<=_ : (a b : Obj A ) → Obj A 
+         _* : {a b c : Obj A } → Hom A (a ∧ b) c → Hom A a (c <= b) 
+         ε : {a b : Obj A } → Hom A ((a <= b ) ∧ b) a 
+         isCCC : IsCCC A １ ○ _∧_ <_,_> π π' _<=_ _* ε 
+
+         Ω : Obj A
+         ⊤ : Hom A １ Ω
+         Ker : {a : Obj A} → ( h : Hom A a Ω ) → Equalizer A h (A [ ⊤ o (○ a) ])
+         char : {a b : Obj A} → ( m : Hom A b a ) → mono A m  → Hom A a Ω
+         isTopos : IsTopos A １ ○ Ker char
+     ker : {a : Obj A} → ( h : Hom A a Ω )  → Hom A ( equalizer-c (Ker h) ) a
+     ker h = equalizer (Ker h)
 
 
 
 
+
+
+
+