|
963
|
1 module ToposEx where
|
|
|
2 open import CCC
|
|
|
3 open import Level
|
|
|
4 open import Category
|
|
|
5 open import cat-utility
|
|
|
6 open import HomReasoning
|
|
|
7
|
|
|
8 open Topos
|
|
|
9 open Equalizer
|
|
|
10
|
|
|
11 -- ○ b
|
|
|
12 -- b -----------→ 1
|
|
|
13 -- | |
|
|
|
14 -- m | | ⊤
|
|
|
15 -- ↓ char m ↓
|
|
|
16 -- a -----------→ Ω
|
|
|
17 -- h
|
|
|
18
|
|
|
19
|
|
|
20 topos-pullback : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) ( １ : Obj A) (○ : (a : Obj A ) → Hom A a １)
|
|
|
21 → (e2 : {a : Obj A} → ∀ { f : Hom A a １ } → A [ f ≈ ○ a ] )
|
|
|
22 → (t : Topos A １ ○ ) → {a : Obj A} → (h : Hom A a (Ω t)) → Pullback A h (⊤ t)
|
|
|
23 topos-pullback A １ ○ e2 t {a} h = record {
|
|
|
24 -- Ker t h : Equalizer A h (A [ ⊤ o (○ a) ])
|
|
|
25 ab = equalizer-c (Ker t h) -- b
|
|
|
26 ; π1 = equalizer (Ker t h) -- m
|
|
|
27 ; π2 = ○ ( equalizer-c (Ker t h) ) -- ○ b
|
|
|
28 ; isPullback = record {
|
|
|
29 commute = comm
|
|
|
30 ; pullback = λ {d} {p1} {p2} eq → IsEqualizer.k (isEqualizer (Ker t h)) p1 (lemma1 p1 p2 eq )
|
|
|
31 ; π1p=π1 = {!!}
|
|
|
32 ; π2p=π2 = {!!}
|
|
|
33 ; uniqueness = {!!}
|
|
|
34 }
|
|
|
35 } where
|
|
|
36 open ≈-Reasoning A
|
|
|
37 comm : A [ A [ h o equalizer (Ker t h) ] ≈ A [ ⊤ t o ○ (equalizer-c (Ker t h)) ] ]
|
|
|
38 comm = begin
|
|
|
39 h o equalizer (Ker t h) ≈⟨ {!!} ⟩
|
|
|
40 ⊤ t o ○ (equalizer-c (Ker t h)) ∎
|
|
|
41 lemma1 : {d : Obj A} (p1 : Hom A d a) (p2 : Hom A d １) (eq : A [ A [ h o p1 ] ≈ A [ ⊤ t o p2 ] ] )
|
|
|
42 → A [ A [ h o p1 ] ≈ A [ A [ ⊤ t o ○ a ] o p1 ] ]
|
|
|
43 lemma1 {d} p1 p2 eq = begin
|
|
|
44 h o p1 ≈⟨ eq ⟩
|
|
|
45 ⊤ t o p2 ≈⟨ cdr e2 ⟩
|
|
|
46 ⊤ t o (○ d) ≈↑⟨ cdr e2 ⟩
|
|
|
47 ⊤ t o ( ○ a o p1 ) ≈⟨ assoc ⟩
|
|
|
48 (⊤ t o ○ a ) o p1 ∎
|
|
|
49
|
