|
963
|
1 open import CCC
|
|
|
2 open import Level
|
|
|
3 open import Category
|
|
|
4 open import cat-utility
|
|
|
5 open import HomReasoning
|
|
974
|
6 module ToposEx {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (c : CCC A) (t : Topos A (CCC.１ c) (CCC.○ c) ) where
|
|
963
|
7
|
|
974
|
8 open Topos
|
|
|
9 open Equalizer
|
|
|
10 open ≈-Reasoning A
|
|
|
11 open CCC.CCC c
|
|
|
12
|
|
963
|
13
|
|
|
14 -- ○ b
|
|
|
15 -- b -----------→ 1
|
|
|
16 -- | |
|
|
|
17 -- m | | ⊤
|
|
|
18 -- ↓ char m ↓
|
|
|
19 -- a -----------→ Ω
|
|
|
20 -- h
|
|
964
|
21 --
|
|
|
22 -- Ker t h : Equalizer A h (A [ ⊤ o (○ a) ])
|
|
963
|
23
|
|
974
|
24 topos-pullback : {a : Obj A} → (h : Hom A a (Ω t)) → Pullback A h (⊤ t)
|
|
|
25 topos-pullback {a} h = record {
|
|
963
|
26 ab = equalizer-c (Ker t h) -- b
|
|
|
27 ; π1 = equalizer (Ker t h) -- m
|
|
|
28 ; π2 = ○ ( equalizer-c (Ker t h) ) -- ○ b
|
|
|
29 ; isPullback = record {
|
|
|
30 commute = comm
|
|
|
31 ; pullback = λ {d} {p1} {p2} eq → IsEqualizer.k (isEqualizer (Ker t h)) p1 (lemma1 p1 p2 eq )
|
|
964
|
32 ; π1p=π1 = IsEqualizer.ek=h (isEqualizer (Ker t h))
|
|
|
33 ; π2p=π2 = λ {d} {p1'} {p2'} {eq} → lemma2 eq
|
|
|
34 ; uniqueness = uniq
|
|
963
|
35 }
|
|
974
|
36 } where
|
|
|
37 e2 = IsCCC.e2 isCCC
|
|
963
|
38 comm : A [ A [ h o equalizer (Ker t h) ] ≈ A [ ⊤ t o ○ (equalizer-c (Ker t h)) ] ]
|
|
|
39 comm = begin
|
|
964
|
40 h o equalizer (Ker t h) ≈⟨ IsEqualizer.fe=ge (isEqualizer (Ker t h)) ⟩
|
|
|
41 (⊤ t o ○ a ) o equalizer (Ker t h) ≈↑⟨ assoc ⟩
|
|
974
|
42 ⊤ t o (○ a o equalizer (Ker t h)) ≈⟨ cdr e2 ⟩
|
|
963
|
43 ⊤ t o ○ (equalizer-c (Ker t h)) ∎
|
|
|
44 lemma1 : {d : Obj A} (p1 : Hom A d a) (p2 : Hom A d １) (eq : A [ A [ h o p1 ] ≈ A [ ⊤ t o p2 ] ] )
|
|
|
45 → A [ A [ h o p1 ] ≈ A [ A [ ⊤ t o ○ a ] o p1 ] ]
|
|
|
46 lemma1 {d} p1 p2 eq = begin
|
|
|
47 h o p1 ≈⟨ eq ⟩
|
|
|
48 ⊤ t o p2 ≈⟨ cdr e2 ⟩
|
|
|
49 ⊤ t o (○ d) ≈↑⟨ cdr e2 ⟩
|
|
|
50 ⊤ t o ( ○ a o p1 ) ≈⟨ assoc ⟩
|
|
|
51 (⊤ t o ○ a ) o p1 ∎
|
|
964
|
52 lemma2 : {d : Obj A} {p1' : Hom A d a} {p2' : Hom A d １} (eq : A [ A [ h o p1' ] ≈ A [ ⊤ t o p2' ] ] )
|
|
|
53 → A [ A [ ○ (equalizer-c (Ker t h)) o IsEqualizer.k (isEqualizer (Ker t h)) p1'(lemma1 p1' p2' eq) ] ≈ p2' ]
|
|
|
54 lemma2 {d} {p1'} {p2'} eq = begin
|
|
|
55 ○ (equalizer-c (Ker t h)) o IsEqualizer.k (isEqualizer (Ker t h)) p1'(lemma1 p1' p2' eq) ≈⟨ e2 ⟩
|
|
|
56 ○ d ≈↑⟨ e2 ⟩
|
|
|
57 p2' ∎
|
|
|
58 uniq : {d : Obj A} (p' : Hom A d (equalizer-c (Ker t h))) {π1' : Hom A d a} {π2' : Hom A d １} {eq : A [ A [ h o π1' ] ≈ A [ ⊤ t o π2' ] ]}
|
|
|
59 {π1p=π1' : A [ A [ equalizer (Ker t h) o p' ] ≈ π1' ]} {π2p=π2' : A [ A [ ○ (equalizer-c (Ker t h)) o p' ] ≈ π2' ]}
|
|
|
60 → A [ IsEqualizer.k (isEqualizer (Ker t h)) π1' (lemma1 π1' π2' eq) ≈ p' ]
|
|
|
61 uniq {d} (p') {p1'} {p2'} {eq} {pe1} {pe2} = begin
|
|
|
62 IsEqualizer.k (isEqualizer (Ker t h)) p1' (lemma1 p1' p2' eq) ≈⟨ IsEqualizer.uniqueness (isEqualizer (Ker t h)) pe1 ⟩
|
|
|
63 p' ∎
|
|
963
|
64
|
|
974
|
65 topos-m-pullback : {a b : Obj A} → (m : Hom A b a) → (mono : Mono A m ) → Pullback A (char t m mono ) (⊤ t)
|
|
|
66 topos-m-pullback {a} {b} m mono = topos-pullback {a} (char t m mono)
|
|
965
|
67
|
|
971
|
68 δmono : {b : Obj A } → Mono A < id1 A b , id1 A b >
|
|
|
69 δmono = record {
|
|
|
70 isMono = m1
|
|
|
71 } where
|
|
|
72 m1 : {d b : Obj A} (f g : Hom A d b) → A [ A [ < id1 A b , id1 A b > o f ] ≈ A [ < id1 A b , id1 A b > o g ] ] → A [ f ≈ g ]
|
|
972
|
73 m1 {d} {b} f g eq = begin
|
|
|
74 f ≈↑⟨ idL ⟩
|
|
|
75 id1 A _ o f ≈↑⟨ car (IsCCC.e3a isCCC) ⟩
|
|
|
76 (π o < id1 A b , id1 A b >) o f ≈↑⟨ assoc ⟩
|
|
|
77 π o (< id1 A b , id1 A b > o f) ≈⟨ cdr eq ⟩
|
|
|
78 π o (< id1 A b , id1 A b > o g) ≈⟨ assoc ⟩
|
|
|
79 (π o < id1 A b , id1 A b >) o g ≈⟨ car (IsCCC.e3a isCCC) ⟩
|
|
|
80 id1 A _ o g ≈⟨ idL ⟩
|
|
|
81 g ∎
|
|
965
|
82
|
|
974
|
83 ip : {b : Obj A } → Pullback A (char t < id1 A b , id1 A b > δmono ) (⊤ t)
|
|
|
84 ip {b} = topos-m-pullback < id1 A b , id1 A b > δmono
|
|
973
|
85
|
|
971
|
86 prop32→ : {a b : Obj A}→ (f g : Hom A a b )
|
|
|
87 → A [ f ≈ g ] → A [ A [ char t < id1 A b , id1 A b > δmono o < f , g > ] ≈ A [ ⊤ t o ○ a ] ]
|
|
972
|
88 prop32→ {a} {b} f g f=g = begin
|
|
|
89 char t < id1 A b , id1 A b > δmono o < f , g > ≈⟨ cdr ( IsCCC.π-cong isCCC refl-hom (sym f=g)) ⟩
|
|
|
90 char t < id1 A b , id1 A b > δmono o < f , f > ≈↑⟨ cdr ( IsCCC.π-cong isCCC idL idL ) ⟩
|
|
|
91 char t < id1 A b , id1 A b > δmono o < id1 A _ o f , id1 A _ o f > ≈↑⟨ cdr ( IsCCC.distr-π isCCC ) ⟩
|
|
|
92 char t < id1 A b , id1 A b > δmono o (< id1 A _ , id1 A _ > o f) ≈⟨ assoc ⟩
|
|
974
|
93 (char t < id1 A b , id1 A b > δmono o Pullback.π1 pb ) o f ≈⟨ car (IsPullback.commute (Pullback.isPullback pb)) ⟩
|
|
972
|
94 (⊤ t o ○ b) o f ≈↑⟨ assoc ⟩
|
|
|
95 ⊤ t o (○ b o f) ≈⟨ cdr (IsCCC.e2 isCCC) ⟩
|
|
973
|
96 ⊤ t o ○ a ∎ where
|
|
974
|
97 pb : Pullback A (char t < id1 A b , id1 A b > δmono) (⊤ t )
|
|
|
98 pb = {!!}
|
|
973
|
99
|
|
971
|
100
|
|
|
101 prop23→ : {a b : Obj A}→ (f g : Hom A a b )
|
|
|
102 → A [ A [ char t < id1 A b , id1 A b > δmono o < f , g > ] ≈ A [ ⊤ t o ○ a ] ] → A [ f ≈ g ]
|
|
|
103 prop23→ = {!!}
|
|
|
104
|
|
|
105 N : (n : ToposNat A １ ) → Obj A
|
|
|
106 N n = NatD.Nat (ToposNat.TNat n)
|
|
|
107
|
|
972
|
108 record prop33 (n : ToposNat A １ ) : Set ( suc c₁ ⊔ suc c₂ ⊔ suc ℓ ) where
|
|
971
|
109 field
|
|
972
|
110 g : {a : Obj A} (f : Hom A １ a ) ( h : Hom A (N n ∧ a) a ) → Hom A (N n) a
|
|
|
111 g0=f : {a : Obj A} (f : Hom A １ a ) ( h : Hom A (N n ∧ a) a ) → A [ A [ g f h o NatD.nzero (ToposNat.TNat n) ] ≈ f ]
|
|
|
112 gs=h : {a : Obj A} (f : Hom A １ a ) ( h : Hom A (N n ∧ a) a ) → A [ A [ g f h o NatD.nsuc (ToposNat.TNat n) ] ≈ A [ h o < id1 A _ , g f h > ] ]
|
|
|
113 g-cong : {a : Obj A} {f f' : Hom A １ a } { h h' : Hom A (N n ∧ a) a } → A [ f ≈ f' ] → A [ h ≈ h' ] → A [ g f h ≈ g f' h' ]
|
|
971
|
114
|
|
|
115 cor33 : (n : ToposNat A １ )
|
|
972
|
116 → prop33 n
|
|
971
|
117 → coProduct A １ ( NatD.Nat (ToposNat.TNat n) ) -- N ≅ N + 1
|
|
|
118 cor33 n p = record {
|
|
|
119 coproduct = N n
|
|
|
120 ; κ1 = NatD.nzero (ToposNat.TNat n)
|
|
972
|
121 ; κ2 = NatD.nsuc (ToposNat.TNat n)
|
|
971
|
122 ; isProduct = record {
|
|
972
|
123 _+_ = λ {a} f g → prop33.g p f ( g o π ) -- Hom A (N n ∧ a) a
|
|
|
124 ; κ1f+g=f = λ {a} {f} {g} → prop33.g0=f p f (g o π )
|
|
|
125 ; κ2f+g=g = k2
|
|
971
|
126 ; uniqueness = {!!}
|
|
972
|
127 ; +-cong = λ f=f' g=g' → prop33.g-cong p f=f' (resp refl-hom g=g' )
|
|
971
|
128
|
|
|
129 }
|
|
972
|
130 } where
|
|
|
131 k2 : {a : Obj A} {f : Hom A １ a} {g : Hom A (NatD.Nat (ToposNat.TNat n)) a }
|
|
|
132 → A [ A [ prop33.g p f ((A Category.o g) π) o NatD.nsuc (ToposNat.TNat n) ] ≈ g ]
|
|
|
133 k2 {a} {f} {g} = begin
|
|
|
134 (prop33.g p f ((A Category.o g) π) o NatD.nsuc (ToposNat.TNat n)) ≈⟨ prop33.gs=h p f (g o π ) ⟩
|
|
|
135 ( g o π ) o < id1 A (N n) , prop33.g p f (g o π) > ≈⟨ sym assoc ⟩
|
|
|
136 g o ( π o < id1 A (N n) , prop33.g p f (g o π) >) ≈⟨ cdr (IsCCC.e3a isCCC ) ⟩
|
|
|
137 g o id1 A (N n) ≈⟨ idR ⟩
|
|
|
138 g ∎
|
|
|
139
|
|
|
140
|
|
|
141
|
