|
963
|
1 open import CCC
|
|
|
2 open import Level
|
|
|
3 open import Category
|
|
|
4 open import cat-utility
|
|
|
5 open import HomReasoning
|
|
1038
|
6 open import Data.List hiding ( [_] )
|
|
|
7 module ToposIL {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (c : CCC A) (t : Topos A c ) (n : ToposNat A (CCC.１ c)) where
|
|
963
|
8
|
|
974
|
9 open Topos
|
|
|
10 open Equalizer
|
|
|
11 open ≈-Reasoning A
|
|
|
12 open CCC.CCC c
|
|
|
13
|
|
1038
|
14 open Functor
|
|
|
15 open import Category.Sets hiding (_o_)
|
|
|
16 open import Relation.Binary.PropositionalEquality hiding ( [_] ; sym)
|
|
963
|
17
|
|
1038
|
18 -- record IsLogic (c : CCC A)
|
|
|
19 -- (Ω : Obj A)
|
|
|
20 -- (⊤ : Hom A (CCC.１ c) Ω)
|
|
|
21 -- (P : Obj A → Obj A)
|
|
|
22 -- (_==_ : {a : Obj A} (x y : Hom A (CCC.１ c) a ) → Hom A ( a ∧ a ) Ω)
|
|
|
23 -- (_∈_ : {a : Obj A} (x : Hom A (CCC.１ c) a ) → Hom A ( a ∧ P a ) Ω)
|
|
|
24 -- (_|-_ : {a : Obj A} (x : List ( Hom A (CCC.１ c) a ) ) → Hom A {!!} Ω)
|
|
|
25 -- : Set ( suc c₁ ⊔ suc c₂ ⊔ suc ℓ ) where
|
|
|
26 -- field
|
|
|
27 -- a : {!!}
|
|
|
28
|
|
|
29 record Logic (c : CCC A) : Set ( suc c₁ ⊔ suc c₂ ⊔ suc ℓ ) where
|
|
|
30 field
|
|
|
31 Ω : Obj A
|
|
|
32 ⊤ : Hom A (CCC.１ c) Ω
|
|
|
33 P : Obj A → Obj A
|
|
|
34 _==_ : {a : Obj A} (x y : Hom A (CCC.１ c) a ) → Hom A (CCC.１ c) Ω
|
|
|
35 _∈_ : {a : Obj A} (x : Hom A (CCC.１ c) a ) (α : Hom A (CCC.１ c) (P a) ) → Hom A (CCC.１ c) Ω
|
|
|
36 _|-_ : {a : Obj A} (x : List ( Hom A (CCC.１ c) a ) ) → Hom A {!!} Ω
|
|
|
37 -- isTL : IsLogic c Ω ⊤ P _==_ _∈_ _|-_
|
|
|
38
|
|
963
|
39 -- ○ b
|
|
|
40 -- b -----------→ 1
|
|
|
41 -- | |
|
|
|
42 -- m | | ⊤
|
|
|
43 -- ↓ char m ↓
|
|
|
44 -- a -----------→ Ω
|
|
971
|
45
|
|
980
|
46 open NatD
|
|
|
47 open ToposNat n
|
|
971
|
48
|
|
980
|
49 N : Obj A
|
|
986
|
50 N = Nat iNat
|
|
980
|
51
|
|
1038
|
52 open import ToposEx A c t n using ( δmono )
|
|
980
|
53
|
|
1038
|
54 topos→logic : Logic c
|
|
|
55 topos→logic = record {
|
|
|
56 Ω = Topos.Ω t
|
|
|
57 ; ⊤ = Topos.⊤ t
|
|
|
58 ; P = {!!}
|
|
|
59 ; _==_ = λ {b} f g → A [ char t < id1 A b , id1 A b > δmono o < f , g > ]
|
|
|
60 ; _∈_ = λ {a} x α → A [ CCC.ε c o < α , x > ]
|
|
|
61 ; _|-_ = {!!}
|
|
|
62 -- ; isTL = {!!}
|
|
|
63 }
|
