Mercurial > hg > Members > kono > Proof > category

changeset 952:61bc4fcba050

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Fri, 19 Feb 2021 11:29:03 +0900
parents ae3551ded289
children eb62812b5885
files src/CCC.agda
diffstat 1 files changed, 22 insertions(+), 20 deletions(-) [+]
line wrap: on
line diff
--- a/src/CCC.agda	Fri Feb 19 09:53:02 2021 +0900
+++ b/src/CCC.agda	Fri Feb 19 11:29:03 2021 +0900
@@ -122,36 +122,38 @@
          ε : {a b : Obj A } → Hom A ((a <= b ) ∧ b) a 
          isCCC : IsCCC A １ ○ _∧_ <_,_> π π' _<=_ _* ε 
 
+----
+--
+-- Sub Object Classifier as Topos
+--
+
 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 Mono  {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) {b a : Obj A} (mono : Hom A b a) : Set  (c₁ ⊔ c₂ ⊔ ℓ)  where
+     field
+         isMono : {c : Obj A} ( f g : Hom A c b ) → A [ A [ mono o f ]  ≈ A [ mono o g ] ] → A [ f ≈ g ]
+
+open Mono
+
+open import equalizer
 
 record IsTopos {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) ( １ : Obj A) (○ : (a : Obj A ) → Hom A 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 Ω) 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
+        (char : {a b : Obj A} → (m :  Hom A b a) → Mono A m  → Hom A a Ω) :  Set ( suc c₁  ⊔  suc c₂ ⊔ suc ℓ ) 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 １ ○ _∧_ <_,_> π π' _<=_ _* ε 
+         char-ker-id  : {a b : Obj A } {h : Hom A a Ω} → (m :  Hom A b a) → (mono : Mono A m)
+             → A [ char (equalizer (Ker h)) record { isMono = {!!} } ≈ h ]
+         ker-char-iso : {a b : Obj A} →  (m :  Hom A b a) → (mono : Mono A m)  → Iso A b (  equalizer-c (Ker ( char m mono ))) 
 
+record Topos {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ)  ( １ : Obj A) (○ : (a : Obj A ) → Hom A a １) :  Set ( suc c₁  ⊔  suc c₂ ⊔ suc ℓ ) where
+     field
          Ω : 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
+         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)