Mercurial > hg > Members > kono > Proof > category

changeset 1046:60b24b3dc0c6

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 Sat, 10 Apr 2021 11:39:46 +0900
parents 139d58917093
children cc7103f643b7
files src/ToposEx.agda src/ToposIL.agda
diffstat 2 files changed, 34 insertions(+), 20 deletions(-) [+]
line wrap: on
line diff
--- a/src/ToposEx.agda	Fri Apr 09 10:26:01 2021 +0900
+++ b/src/ToposEx.agda	Sat Apr 10 11:39:46 2021 +0900
@@ -366,6 +366,19 @@
   partialmapClassifier : (b : Obj A) → PartialmapClassifier b
   partialmapClassifier = {!!}
 
+  record SubObject (a : Obj A) : Set (c₁ ⊔ c₂ ⊔ ℓ)  where
+     field
+        sb : Obj A
+        sm : Hom A sb a 
+        smono : Mono A sm
+
+  record SubObjectClassifier  (b : Obj A) :  Set (c₁ ⊔ c₂ ⊔ ℓ) where
+      field
+         sm : SubObject b
+         smc : {a : Obj A} ( d f : Hom A a b) → Mono A d → Hom A a b
+         pb : {a : Obj A} ( d f : Hom A a b) → (dm : Mono A d ) → Pullback A (smc d f dm) (id1 A _) 
+         uniq : {a : Obj A} ( d f : Hom A a b) → (dm : Mono A d ) → (p : Hom A a b) → Pullback A p (id1 A _) → A [ smc d f dm ≈ p ]
+
   postulate
     I : Set c₁
     small : Small A I 
--- a/src/ToposIL.agda	Fri Apr 09 10:26:01 2021 +0900
+++ b/src/ToposIL.agda	Sat Apr 10 11:39:46 2021 +0900
@@ -17,25 +17,26 @@
 
   -- record IsLogic    (c : CCC A) 
   --        (Ω : Obj A)
-  --        (⊤ : Hom A (CCC.１ c) Ω)
+  --        (⊤ : Hom A １ Ω)
   --        (P  : Obj A → Obj A)
-  --        (_==_ : {a : Obj A} (x y : Hom A  (CCC.１ c) a ) → Hom A ( a ∧ a ) Ω)
-  --        (_∈_ : {a : Obj A} (x : Hom A (CCC.１ c) a ) → Hom A ( a ∧ P a ) Ω)
-  --        (_|-_  : {a : Obj A} (x : List ( Hom A (CCC.１ c) a ) ) → Hom A {!!} Ω)
+  --        (_==_ : {a : Obj A} (x y : Hom A １ a ) → Hom A ( a ∧ a ) Ω)
+  --        (_∈_ : {a : Obj A} (x : Hom A １ a ) → Hom A ( a ∧ P a ) Ω)
+  --        (_|-_  : {a : Obj A} (x : List ( Hom A １ a ) ) → Hom A {!!} Ω)
   --           :   Set ( suc c₁  ⊔  suc c₂ ⊔ suc ℓ ) where
   --    field
   --        a : {!!}
 
-  record InternalLanguage (Ω : Obj A) (⊤ : Hom A (CCC.１ c) Ω) (P  : Obj A → Obj A)
+  record InternalLanguage (Ω : Obj A) (⊤ : Hom A １ Ω) (P  : Obj A → Obj A)
           :   Set ( suc c₁  ⊔  suc c₂ ⊔ suc ℓ ) where
      field
-         _==_ : {a : Obj A} (x y : Hom A  (CCC.１ c) a ) → Hom A (CCC.１ c) Ω
-         _∈_ : {a : Obj A} (x :  Hom A  (CCC.１ c) a ) (α : Hom A (CCC.１ c) (P a) ) → Hom A (CCC.１ c) Ω
+         _==_ : {a : Obj A} (x y : Hom A １ a ) → Hom A １ Ω
+         _∈_ : {a : Obj A} (x :  Hom A １ a ) (α : Hom A １ (P a) ) → Hom A １ Ω
          -- { x ∈ a | φ x } : P a
-         select : {a b : Obj A}  (α : Hom A (CCC.１ c) (P a) ) → ( (x :  Hom A  (CCC.１ c) a ) →  Hom A (CCC.１ c) Ω ) → Hom A (CCC.１ c) (P a)
+         select : {a : Obj A} → ( (x :  Hom A １ a ) →  Hom A １ Ω ) → Hom A １ (P a)
          -- isTL : IsLogic c Ω ⊤ P _==_ _∈_  _|-_
-     |-_  : {a : Obj A} (p : Hom A (CCC.１ c) Ω ) → Set ℓ
-     |-_  {a} p = A [ p ≈  ⊤ ] 
+     _|-_  :  (List (Hom A １ Ω)) → (p : Hom A １ Ω ) → Set ℓ
+     [] |-  p = A [ p ≈  ⊤ ] 
+     (h ∷ t) |-  p = {!!}
   
 --             ○ b
 --       b -----------→ 1
@@ -44,7 +45,7 @@
 --       ↓    char m    ↓
 --       a -----------→ Ω
 
-  -- (n : ToposNat A (CCC.１ c))
+  -- (n : ToposNat A １)
   -- open NatD
   -- open ToposNat n
 
@@ -54,23 +55,23 @@
   open import ToposEx A c using ( δmono  )
 
   -- f ≡ λ (x ∈ a) → φ x or  ∃ (f : b <= a) →  f ∙ x ≈  φ x  
-  record Select  {a b : Obj A} (Ω : Obj A) (α : Hom A (CCC.１ c) (Ω <= a) ) ( φ : (x :  Hom A  (CCC.１ c) a ) → Hom A (CCC.１ c) b )
+  record Select  {a b : Obj A} (Ω : Obj A) ( φ : (x :  Hom A １ a ) → Hom A １ b )
          :  Set ( suc c₁  ⊔  suc c₂ ⊔ suc ℓ ) where
     field
-      sl :  Hom A (CCC.１ c) (b <= a) 
-      isSelect : (x : Hom A  (CCC.１ c) a  ) → A [  A [ CCC.ε c o < sl , x > ]  ≈  φ x ]
-      -- isUnique : (x : Hom A  (CCC.１ c) a  ) → (f : Hom A (CCC.１ c) (b <= a) )  → A [  A [ CCC.ε c o < f , x > ]  ≈  φ x ]
-      --   →  A [ sl  ≈ f ]
+      sl :  Hom A １ (b <= a) 
+      isSelect : (x : Hom A １ a  ) → A [  A [ ε o < sl , x > ]  ≈  φ x ]
+      isUnique : (x : Hom A １ a  ) → (f : Hom A １ (b <= a) )  → A [  A [ ε o < f , x > ]  ≈  φ x ]
+        →  A [ sl  ≈ f ]
 
   -- functional completeness
   FC : Set ( suc c₁  ⊔  suc c₂ ⊔ suc ℓ )
-  FC = {a b : Obj A}  (α : Hom A (CCC.１ c) (b <= a) ) ( φ : (x :  Hom A  (CCC.１ c) a ) → Hom A (CCC.１ c) b ) → Select b α φ
+  FC = {a b : Obj A}  ( φ : (x :  Hom A １ a ) → Hom A １ b ) → Select b φ
 
-  topos→logic : (t : Topos A c ) → ToposNat A (CCC.１ c)  → FC  → InternalLanguage (Topos.Ω t) (Topos.⊤ t) (λ a → (Topos.Ω t) <= a)
+  topos→logic : (t : Topos A c ) → ToposNat A １ → FC  → InternalLanguage (Topos.Ω t) (Topos.⊤ t) (λ a → (Topos.Ω t) <= a)
   topos→logic t n fc = record {
          _==_ = λ {b} f g →   A [ char t < id1 A b , id1 A b > (δmono t n ) o < f , g > ]
-      ;  _∈_ = λ {a} x α →  A [ CCC.ε c o < α , x > ]
+      ;  _∈_ = λ {a} x α →  A [ ε o < α , x > ]
       -- { x ∈ a | φ x } : P a
-      ;  select = λ {a} α φ →  Select.sl ( fc α φ )
+      ;  select = λ {a} φ →  Select.sl ( fc φ )
       -- ;  isTL = {!!}
     }