|
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
|
|
964
|
18 --
|
|
|
19 -- Ker t h : Equalizer A h (A [ ⊤ o (○ a) ])
|
|
963
|
20
|
|
|
21 topos-pullback : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) ( １ : Obj A) (○ : (a : Obj A ) → Hom A a １)
|
|
|
22 → (e2 : {a : Obj A} → ∀ { f : Hom A a １ } → A [ f ≈ ○ a ] )
|
|
|
23 → (t : Topos A １ ○ ) → {a : Obj A} → (h : Hom A a (Ω t)) → Pullback A h (⊤ t)
|
|
|
24 topos-pullback A １ ○ e2 t {a} h = record {
|
|
|
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 )
|
|
964
|
31 ; π1p=π1 = IsEqualizer.ek=h (isEqualizer (Ker t h))
|
|
|
32 ; π2p=π2 = λ {d} {p1'} {p2'} {eq} → lemma2 eq
|
|
|
33 ; uniqueness = uniq
|
|
963
|
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
|
|
964
|
39 h o equalizer (Ker t h) ≈⟨ IsEqualizer.fe=ge (isEqualizer (Ker t h)) ⟩
|
|
|
40 (⊤ t o ○ a ) o equalizer (Ker t h) ≈↑⟨ assoc ⟩
|
|
|
41 ⊤ t o (○ a o equalizer (Ker t h)) ≈⟨ cdr e2 ⟩
|
|
963
|
42 ⊤ t o ○ (equalizer-c (Ker t h)) ∎
|
|
|
43 lemma1 : {d : Obj A} (p1 : Hom A d a) (p2 : Hom A d １) (eq : A [ A [ h o p1 ] ≈ A [ ⊤ t o p2 ] ] )
|
|
|
44 → A [ A [ h o p1 ] ≈ A [ A [ ⊤ t o ○ a ] o p1 ] ]
|
|
|
45 lemma1 {d} p1 p2 eq = begin
|
|
|
46 h o p1 ≈⟨ eq ⟩
|
|
|
47 ⊤ t o p2 ≈⟨ cdr e2 ⟩
|
|
|
48 ⊤ t o (○ d) ≈↑⟨ cdr e2 ⟩
|
|
|
49 ⊤ t o ( ○ a o p1 ) ≈⟨ assoc ⟩
|
|
|
50 (⊤ t o ○ a ) o p1 ∎
|
|
964
|
51 lemma2 : {d : Obj A} {p1' : Hom A d a} {p2' : Hom A d １} (eq : A [ A [ h o p1' ] ≈ A [ ⊤ t o p2' ] ] )
|
|
|
52 → A [ A [ ○ (equalizer-c (Ker t h)) o IsEqualizer.k (isEqualizer (Ker t h)) p1'(lemma1 p1' p2' eq) ] ≈ p2' ]
|
|
|
53 lemma2 {d} {p1'} {p2'} eq = begin
|
|
|
54 ○ (equalizer-c (Ker t h)) o IsEqualizer.k (isEqualizer (Ker t h)) p1'(lemma1 p1' p2' eq) ≈⟨ e2 ⟩
|
|
|
55 ○ d ≈↑⟨ e2 ⟩
|
|
|
56 p2' ∎
|
|
|
57 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' ] ]}
|
|
|
58 {π1p=π1' : A [ A [ equalizer (Ker t h) o p' ] ≈ π1' ]} {π2p=π2' : A [ A [ ○ (equalizer-c (Ker t h)) o p' ] ≈ π2' ]}
|
|
|
59 → A [ IsEqualizer.k (isEqualizer (Ker t h)) π1' (lemma1 π1' π2' eq) ≈ p' ]
|
|
|
60 uniq {d} (p') {p1'} {p2'} {eq} {pe1} {pe2} = begin
|
|
|
61 IsEqualizer.k (isEqualizer (Ker t h)) p1' (lemma1 p1' p2' eq) ≈⟨ IsEqualizer.uniqueness (isEqualizer (Ker t h)) pe1 ⟩
|
|
|
62 p' ∎
|
|
963
|
63
|
|
965
|
64 topos-m-pullback : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) ( １ : Obj A) (○ : (a : Obj A ) → Hom A a １)
|
|
|
65 → (e2 : {a : Obj A} → ∀ { f : Hom A a １ } → A [ f ≈ ○ a ] )
|
|
|
66 → (t : Topos A １ ○ ) → {a b : Obj A} → (m : Hom A b a) → (mono : Mono A m ) → Pullback A (char t m mono ) (⊤ t)
|
|
|
67 topos-m-pullback A １ ○ e2 t {a} {b} m mono = topos-pullback A １ ○ e2 t {a} (char t m mono)
|
|
964
|
68
|
|
965
|
69 ---
|
|
|
70 ---
|
|
|
71 ---
|
|
|
72
|
|
|
73 -- SubObjectFunctor : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) → ( １ : Obj A) (○ : (a : Obj A ) → Hom A a １)
|
|
|
74 -- → (e2 : {a : Obj A} → ∀ { f : Hom A a １ } → A [ f ≈ ○ a ] ) → (t : Topos A １ ○ ) → Functor A A
|
|
|
75 -- SubObjectFunctor A １ ○ e2 t = record {
|
|
|
76 -- FObj = λ x → Ω t
|
|
|
77 -- ; FMap = {!!}
|
|
|
78 -- ; isFunctor = record {
|
|
|
79 -- identity = {!!}
|
|
|
80 -- ; distr = {!!}
|
|
|
81 -- ; ≈-cong = {!!}
|
|
|
82 -- }
|
|
|
83 -- }
|
|
|
84
|
|
|
85
|
|
|
86
|
