|
779
|
1 open import Level
|
|
950
|
2 open import Category
|
|
779
|
3 module CCC where
|
|
|
4
|
|
950
|
5
|
|
779
|
6 open import HomReasoning
|
|
|
7 open import cat-utility
|
|
780
|
8 open import Relation.Binary.PropositionalEquality
|
|
779
|
9
|
|
783
|
10
|
|
|
11 open import HomReasoning
|
|
|
12
|
|
784
|
13 record IsCCC {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ)
|
|
783
|
14 ( １ : Obj A )
|
|
|
15 ( ○ : (a : Obj A ) → Hom A a １ )
|
|
|
16 ( _∧_ : Obj A → Obj A → Obj A )
|
|
|
17 ( <_,_> : {a b c : Obj A } → Hom A c a → Hom A c b → Hom A c (a ∧ b) )
|
|
|
18 ( π : {a b : Obj A } → Hom A (a ∧ b) a )
|
|
|
19 ( π' : {a b : Obj A } → Hom A (a ∧ b) b )
|
|
|
20 ( _<=_ : (a b : Obj A ) → Obj A )
|
|
|
21 ( _* : {a b c : Obj A } → Hom A (a ∧ b) c → Hom A a (c <= b) )
|
|
|
22 ( ε : {a b : Obj A } → Hom A ((a <= b ) ∧ b) a )
|
|
|
23 : Set ( c₁ ⊔ c₂ ⊔ ℓ ) where
|
|
|
24 field
|
|
|
25 -- cartesian
|
|
793
|
26 e2 : {a : Obj A} → ∀ { f : Hom A a １ } → A [ f ≈ ○ a ]
|
|
783
|
27 e3a : {a b c : Obj A} → { f : Hom A c a }{ g : Hom A c b } → A [ A [ π o < f , g > ] ≈ f ]
|
|
|
28 e3b : {a b c : Obj A} → { f : Hom A c a }{ g : Hom A c b } → A [ A [ π' o < f , g > ] ≈ g ]
|
|
|
29 e3c : {a b c : Obj A} → { h : Hom A c (a ∧ b) } → A [ < A [ π o h ] , A [ π' o h ] > ≈ h ]
|
|
785
|
30 π-cong : {a b c : Obj A} → { f f' : Hom A c a }{ g g' : Hom A c b } → A [ f ≈ f' ] → A [ g ≈ g' ] → A [ < f , g > ≈ < f' , g' > ]
|
|
783
|
31 -- closed
|
|
|
32 e4a : {a b c : Obj A} → { h : Hom A (c ∧ b) a } → A [ A [ ε o < A [ (h *) o π ] , π' > ] ≈ h ]
|
|
|
33 e4b : {a b c : Obj A} → { k : Hom A c (a <= b ) } → A [ ( A [ ε o < A [ k o π ] , π' > ] ) * ≈ k ]
|
|
787
|
34 *-cong : {a b c : Obj A} → { f f' : Hom A (a ∧ b) c } → A [ f ≈ f' ] → A [ f * ≈ f' * ]
|
|
779
|
35
|
|
783
|
36 e'2 : A [ ○ １ ≈ id1 A １ ]
|
|
|
37 e'2 = let open ≈-Reasoning A in begin
|
|
|
38 ○ １
|
|
793
|
39 ≈↑⟨ e2 ⟩
|
|
783
|
40 id1 A １
|
|
|
41 ∎
|
|
|
42 e''2 : {a b : Obj A} {f : Hom A a b } → A [ A [ ○ b o f ] ≈ ○ a ]
|
|
|
43 e''2 {a} {b} {f} = let open ≈-Reasoning A in begin
|
|
|
44 ○ b o f
|
|
793
|
45 ≈⟨ e2 ⟩
|
|
783
|
46 ○ a
|
|
|
47 ∎
|
|
789
|
48 π-id : {a b : Obj A} → A [ < π , π' > ≈ id1 A (a ∧ b ) ]
|
|
|
49 π-id {a} {b} = let open ≈-Reasoning A in begin
|
|
|
50 < π , π' >
|
|
|
51 ≈↑⟨ π-cong idR idR ⟩
|
|
|
52 < π o id1 A (a ∧ b) , π' o id1 A (a ∧ b) >
|
|
|
53 ≈⟨ e3c ⟩
|
|
|
54 id1 A (a ∧ b )
|
|
|
55 ∎
|
|
794
|
56 distr-π : {a b c d : Obj A} {f : Hom A c a }{g : Hom A c b } {h : Hom A d c } → A [ A [ < f , g > o h ] ≈ < A [ f o h ] , A [ g o h ] > ]
|
|
|
57 distr-π {a} {b} {c} {d} {f} {g} {h} = let open ≈-Reasoning A in begin
|
|
783
|
58 < f , g > o h
|
|
|
59 ≈↑⟨ e3c ⟩
|
|
|
60 < π o < f , g > o h , π' o < f , g > o h >
|
|
785
|
61 ≈⟨ π-cong assoc assoc ⟩
|
|
|
62 < ( π o < f , g > ) o h , (π' o < f , g > ) o h >
|
|
|
63 ≈⟨ π-cong (car e3a ) (car e3b) ⟩
|
|
783
|
64 < f o h , g o h >
|
|
|
65 ∎
|
|
794
|
66 _×_ : { a b c d : Obj A } ( f : Hom A a c ) (g : Hom A b d ) → Hom A (a ∧ b) ( c ∧ d )
|
|
|
67 f × g = < (A [ f o π ] ) , (A [ g o π' ]) >
|
|
|
68 distr-* : {a b c d : Obj A } { h : Hom A (a ∧ b) c } { k : Hom A d a } → A [ A [ h * o k ] ≈ ( A [ h o < A [ k o π ] , π' > ] ) * ]
|
|
|
69 distr-* {a} {b} {c} {d} {h} {k} = begin
|
|
|
70 h * o k
|
|
|
71 ≈↑⟨ e4b ⟩
|
|
|
72 ( ε o < (h * o k ) o π , π' > ) *
|
|
|
73 ≈⟨ *-cong ( begin
|
|
|
74 ε o < (h * o k ) o π , π' >
|
|
|
75 ≈↑⟨ cdr ( π-cong assoc refl-hom ) ⟩
|
|
|
76 ε o ( < h * o ( k o π ) , π' > )
|
|
|
77 ≈↑⟨ cdr ( π-cong (cdr e3a) e3b ) ⟩
|
|
|
78 ε o ( < h * o ( π o < k o π , π' > ) , π' o < k o π , π' > > )
|
|
|
79 ≈⟨ cdr ( π-cong assoc refl-hom) ⟩
|
|
|
80 ε o ( < (h * o π) o < k o π , π' > , π' o < k o π , π' > > )
|
|
|
81 ≈↑⟨ cdr ( distr-π ) ⟩
|
|
|
82 ε o ( < h * o π , π' > o < k o π , π' > )
|
|
|
83 ≈⟨ assoc ⟩
|
|
|
84 ( ε o < h * o π , π' > ) o < k o π , π' >
|
|
|
85 ≈⟨ car e4a ⟩
|
|
|
86 h o < k o π , π' >
|
|
|
87 ∎ ) ⟩
|
|
|
88 ( h o < k o π , π' > ) *
|
|
|
89 ∎ where open ≈-Reasoning A
|
|
|
90 α : {a b c : Obj A } → Hom A (( a ∧ b ) ∧ c ) ( a ∧ ( b ∧ c ) )
|
|
|
91 α = < A [ π o π ] , < A [ π' o π ] , π' > >
|
|
|
92 α' : {a b c : Obj A } → Hom A ( a ∧ ( b ∧ c ) ) (( a ∧ b ) ∧ c )
|
|
|
93 α' = < < π , A [ π o π' ] > , A [ π' o π' ] >
|
|
|
94 β : {a b c d : Obj A } { f : Hom A a b} { g : Hom A a c } { h : Hom A a d } → A [ A [ α o < < f , g > , h > ] ≈ < f , < g , h > > ]
|
|
|
95 β {a} {b} {c} {d} {f} {g} {h} = begin
|
|
|
96 α o < < f , g > , h >
|
|
|
97 ≈⟨⟩
|
|
|
98 ( < ( π o π ) , < ( π' o π ) , π' > > ) o < < f , g > , h >
|
|
|
99 ≈⟨ distr-π ⟩
|
|
|
100 < ( ( π o π ) o < < f , g > , h > ) , ( < ( π' o π ) , π' > o < < f , g > , h > ) >
|
|
|
101 ≈⟨ π-cong refl-hom distr-π ⟩
|
|
|
102 < ( ( π o π ) o < < f , g > , h > ) , ( < ( ( π' o π ) o < < f , g > , h > ) , ( π' o < < f , g > , h > ) > ) >
|
|
|
103 ≈↑⟨ π-cong assoc ( π-cong assoc refl-hom ) ⟩
|
|
|
104 < ( π o (π o < < f , g > , h >) ) , ( < ( π' o ( π o < < f , g > , h > ) ) , ( π' o < < f , g > , h > ) > ) >
|
|
|
105 ≈⟨ π-cong (cdr e3a ) ( π-cong (cdr e3a ) e3b ) ⟩
|
|
|
106 < ( π o < f , g > ) , < ( π' o < f , g > ) , h > >
|
|
|
107 ≈⟨ π-cong e3a ( π-cong e3b refl-hom ) ⟩
|
|
|
108 < f , < g , h > >
|
|
|
109 ∎ where open ≈-Reasoning A
|
|
|
110
|
|
783
|
111
|
|
784
|
112 record CCC {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) : Set ( c₁ ⊔ c₂ ⊔ ℓ ) where
|
|
781
|
113 field
|
|
783
|
114 １ : Obj A
|
|
|
115 ○ : (a : Obj A ) → Hom A a １
|
|
|
116 _∧_ : Obj A → Obj A → Obj A
|
|
|
117 <_,_> : {a b c : Obj A } → Hom A c a → Hom A c b → Hom A c (a ∧ b)
|
|
|
118 π : {a b : Obj A } → Hom A (a ∧ b) a
|
|
|
119 π' : {a b : Obj A } → Hom A (a ∧ b) b
|
|
|
120 _<=_ : (a b : Obj A ) → Obj A
|
|
|
121 _* : {a b c : Obj A } → Hom A (a ∧ b) c → Hom A a (c <= b)
|
|
|
122 ε : {a b : Obj A } → Hom A ((a <= b ) ∧ b) a
|
|
784
|
123 isCCC : IsCCC A １ ○ _∧_ <_,_> π π' _<=_ _* ε
|
|
781
|
124
|
|
952
|
125 ----
|
|
|
126 --
|
|
|
127 -- Sub Object Classifier as Topos
|
|
|
128 --
|
|
|
129
|
|
950
|
130 open Equalizer
|
|
|
131
|
|
952
|
132 record Mono {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) {b a : Obj A} (mono : Hom A b a) : Set (c₁ ⊔ c₂ ⊔ ℓ) where
|
|
|
133 field
|
|
|
134 isMono : {c : Obj A} ( f g : Hom A c b ) → A [ A [ mono o f ] ≈ A [ mono o g ] ] → A [ f ≈ g ]
|
|
|
135
|
|
|
136 open Mono
|
|
|
137
|
|
|
138 open import equalizer
|
|
950
|
139
|
|
|
140 record IsTopos {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) ( １ : Obj A) (○ : (a : Obj A ) → Hom A a １)
|
|
952
|
141 ( Ω : Obj A )
|
|
|
142 ( ⊤ : Hom A １ Ω )
|
|
950
|
143 (Ker : {a : Obj A} → ( h : Hom A a Ω ) → Equalizer A h (A [ ⊤ o (○ a) ]))
|
|
952
|
144 (char : {a b : Obj A} → (m : Hom A b a) → Mono A m → Hom A a Ω) : Set ( suc c₁ ⊔ suc c₂ ⊔ suc ℓ ) where
|
|
950
|
145 field
|
|
952
|
146 char-ker-id : {a b : Obj A } {h : Hom A a Ω} → (m : Hom A b a) → (mono : Mono A m)
|
|
953
|
147 → A [ char (equalizer (Ker h)) record { isMono = monic (Ker h) } ≈ h ]
|
|
952
|
148 ker-char-iso : {a b : Obj A} → (m : Hom A b a) → (mono : Mono A m) → Iso A b ( equalizer-c (Ker ( char m mono )))
|
|
950
|
149
|
|
952
|
150 record Topos {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) ( １ : Obj A) (○ : (a : Obj A ) → Hom A a １) : Set ( suc c₁ ⊔ suc c₂ ⊔ suc ℓ ) where
|
|
|
151 field
|
|
950
|
152 Ω : Obj A
|
|
|
153 ⊤ : Hom A １ Ω
|
|
|
154 Ker : {a : Obj A} → ( h : Hom A a Ω ) → Equalizer A h (A [ ⊤ o (○ a) ])
|
|
952
|
155 char : {a b : Obj A} → (m : Hom A b a ) → Mono A m → Hom A a Ω
|
|
|
156 isTopos : IsTopos A １ ○ Ω ⊤ Ker char
|
|
950
|
157 ker : {a : Obj A} → ( h : Hom A a Ω ) → Hom A ( equalizer-c (Ker h) ) a
|
|
|
158 ker h = equalizer (Ker h)
|
|
783
|
159
|
|
|
160
|
|
|
161
|
|
|
162
|
|
950
|
163
|
|
|
164
|
|
|
165
|
|
|
166
|
