|
776
|
1 open import Category -- https://github.com/konn/category-agda
|
|
|
2 open import Level
|
|
|
3
|
|
|
4 module epi where
|
|
|
5
|
|
|
6 open import Relation.Binary.Core
|
|
|
7
|
|
|
8 data FourObject : Set where
|
|
|
9 ta : FourObject
|
|
|
10 tb : FourObject
|
|
|
11 tc : FourObject
|
|
|
12 td : FourObject
|
|
|
13
|
|
|
14 data FourHom : FourObject → FourObject → Set where
|
|
|
15 id-ta : FourHom ta ta
|
|
|
16 id-tb : FourHom tb tb
|
|
|
17 id-tc : FourHom tc tc
|
|
|
18 id-td : FourHom td td
|
|
|
19 arrow-ca : FourHom tc ta
|
|
|
20 arrow-ab : FourHom ta tb
|
|
|
21 arrow-bd : FourHom tb td
|
|
|
22 arrow-cb : FourHom tc tb
|
|
|
23 arrow-ad : FourHom ta td
|
|
|
24 arrow-cd : FourHom tc td
|
|
|
25
|
|
|
26
|
|
|
27 _×_ : {a b c : FourObject } → FourHom b c → FourHom a b → FourHom a c
|
|
|
28 _×_ {x} {ta} {ta} id-ta y = y
|
|
|
29 _×_ {x} {tb} {tb} id-tb y = y
|
|
|
30 _×_ {x} {tc} {tc} id-tc y = y
|
|
|
31 _×_ {x} {td} {td} id-td y = y
|
|
|
32 _×_ {ta} {ta} {x} y id-ta = y
|
|
|
33 _×_ {tb} {tb} {x} y id-tb = y
|
|
|
34 _×_ {tc} {tc} {x} y id-tc = y
|
|
|
35 _×_ {td} {td} {x} y id-td = y
|
|
|
36 _×_ {tc} {ta} {tb} arrow-ab arrow-ca = arrow-cb
|
|
|
37 _×_ {ta} {tb} {td} arrow-bd arrow-ab = arrow-ad
|
|
|
38 _×_ {tc} {tb} {td} arrow-bd arrow-cb = arrow-cd
|
|
|
39 _×_ {tc} {ta} {td} arrow-ad arrow-ca = arrow-cd
|
|
|
40 _×_ {tc} {ta} {tc} () arrow-ca
|
|
|
41 _×_ {ta} {tb} {ta} () arrow-ab
|
|
|
42 _×_ {tc} {tb} {ta} () arrow-cb
|
|
|
43 _×_ {ta} {tb} {tc} () arrow-ab
|
|
|
44 _×_ {tc} {tb} {tc} () arrow-cb
|
|
|
45 _×_ {tb} {td} {ta} () arrow-bd
|
|
|
46 _×_ {ta} {td} {ta} () arrow-ad
|
|
|
47 _×_ {tc} {td} {ta} () arrow-cd
|
|
|
48 _×_ {tb} {td} {tb} () arrow-bd
|
|
|
49 _×_ {ta} {td} {tb} () arrow-ad
|
|
|
50 _×_ {tc} {td} {tb} () arrow-cd
|
|
|
51 _×_ {tb} {td} {tc} () arrow-bd
|
|
|
52 _×_ {ta} {td} {tc} () arrow-ad
|
|
|
53 _×_ {tc} {td} {tc} () arrow-cd
|
|
|
54
|
|
|
55 open FourHom
|
|
|
56
|
|
|
57
|
|
|
58 assoc-× : {a b c d : FourObject }
|
|
|
59 {f : (FourHom c d )} → {g : (FourHom b c )} → {h : (FourHom a b )} →
|
|
|
60 ( f × (g × h)) ≡ ((f × g) × h )
|
|
|
61 assoc-× {_} {_} {_} {_} {id-ta} {y} {z} = refl
|
|
|
62 assoc-× {_} {_} {_} {_} {id-tb} {y} {z} = refl
|
|
|
63 assoc-× {_} {_} {_} {_} {id-tc} {y} {z} = refl
|
|
|
64 assoc-× {_} {_} {_} {_} {id-td} {y} {z} = refl
|
|
|
65 assoc-× {_} {_} {_} {_} {arrow-ca} {id-tc} {z} = refl
|
|
|
66 assoc-× {_} {_} {_} {_} {arrow-ab} {id-ta} {z} = refl
|
|
|
67 assoc-× {_} {_} {_} {_} {arrow-ab} {arrow-ca} {id-tc} = refl
|
|
|
68 assoc-× {_} {_} {_} {_} {arrow-bd} {id-tb} {z} = refl
|
|
|
69 assoc-× {_} {_} {_} {_} {arrow-bd} {arrow-ab} {id-ta} = refl
|
|
|
70 assoc-× {_} {_} {_} {_} {arrow-bd} {arrow-ab} {arrow-ca} = refl
|
|
|
71 assoc-× {_} {_} {_} {_} {arrow-bd} {arrow-cb} {id-tc} = refl
|
|
|
72 assoc-× {_} {_} {_} {_} {arrow-cb} {id-tc} {z} = refl
|
|
|
73 assoc-× {_} {_} {_} {_} {arrow-ad} {id-ta} {z} = refl
|
|
|
74 assoc-× {_} {_} {_} {_} {arrow-ad} {arrow-ca} {id-tc} = refl
|
|
|
75 assoc-× {_} {_} {_} {_} {arrow-cd} {id-tc} {id-tc} = refl
|
|
|
76
|
|
|
77 FourId : (a : FourObject ) → (FourHom a a )
|
|
|
78 FourId ta = id-ta
|
|
|
79 FourId tb = id-tb
|
|
|
80 FourId tc = id-tc
|
|
|
81 FourId td = id-td
|
|
|
82
|
|
|
83 open import Relation.Binary.PropositionalEquality
|
|
|
84
|
|
|
85 FourCat : Category zero zero zero
|
|
|
86 FourCat = record {
|
|
|
87 Obj = FourObject ;
|
|
|
88 Hom = λ a b → FourHom a b ;
|
|
|
89 _o_ = λ{a} {b} {c} x y → _×_ x y ;
|
|
|
90 _≈_ = λ x y → x ≡ y ;
|
|
|
91 Id = λ{a} → FourId a ;
|
|
|
92 isCategory = record {
|
|
|
93 isEquivalence = record {refl = refl ; trans = trans ; sym = sym } ; identityL = λ{a b f} → identityL {a} {b} {f} ;
|
|
|
94 identityR = λ{a b f} → identityR {a} {b} {f} ;
|
|
|
95 o-resp-≈ = λ{a b c f g h i} → o-resp-≈ {a} {b} {c} {f} {g} {h} {i} ;
|
|
|
96 associative = λ{a b c d f g h } → assoc-× {a} {b} {c} {d} {f} {g} {h}
|
|
|
97 }
|
|
|
98 } where
|
|
|
99 identityL : {A B : FourObject } {f : ( FourHom A B) } → ((FourId B) × f) ≡ f
|
|
|
100 identityL {ta} {ta} {id-ta} = refl
|
|
|
101 identityL {tb} {tb} {id-tb} = refl
|
|
|
102 identityL {tc} {tc} {id-tc} = refl
|
|
|
103 identityL {td} {td} {id-td} = refl
|
|
|
104 identityL {tc} {ta} {arrow-ca} = refl
|
|
|
105 identityL {ta} {tb} {arrow-ab} = refl
|
|
|
106 identityL {tb} {td} {arrow-bd} = refl
|
|
|
107 identityL {tc} {tb} {arrow-cb} = refl
|
|
|
108 identityL {ta} {td} {arrow-ad} = refl
|
|
|
109 identityL {tc} {td} {arrow-cd} = refl
|
|
|
110 identityR : {A B : FourObject } {f : ( FourHom A B) } → ( f × FourId A ) ≡ f
|
|
|
111 identityR {ta} {ta} {id-ta} = refl
|
|
|
112 identityR {tb} {tb} {id-tb} = refl
|
|
|
113 identityR {tc} {tc} {id-tc} = refl
|
|
|
114 identityR {td} {td} {id-td} = refl
|
|
|
115 identityR {tc} {ta} {arrow-ca} = refl
|
|
|
116 identityR {ta} {tb} {arrow-ab} = refl
|
|
|
117 identityR {tb} {td} {arrow-bd} = refl
|
|
|
118 identityR {tc} {tb} {arrow-cb} = refl
|
|
|
119 identityR {ta} {td} {arrow-ad} = refl
|
|
|
120 identityR {tc} {td} {arrow-cd} = refl
|
|
|
121 o-resp-≈ : {A B C : FourObject } {f g : ( FourHom A B)} {h i : ( FourHom B C)} →
|
|
|
122 f ≡ g → h ≡ i → ( h × f ) ≡ ( i × g )
|
|
|
123 o-resp-≈ {a} {b} {c} {f} {x} {h} {y} refl refl = refl
|
|
|
124
|
|
|
125 epi : {a b c : FourObject } {f₁ f₂ : Hom FourCat a b } { h : Hom FourCat b c }
|
|
|
126 → FourCat [ h o f₁ ] ≡ FourCat [ h o f₂ ] → f₁ ≡ f₂
|
|
|
127 epi {ta} {ta} {c} {id-ta} {id-ta} {h} refl = refl
|
|
|
128 epi {tb} {tb} {c} {id-tb} {id-tb} {h} refl = refl
|
|
|
129 epi {tc} {tc} {c} {id-tc} {id-tc} {h} refl = refl
|
|
|
130 epi {td} {td} {c} {id-td} {id-td} {h} refl = refl
|
|
|
131 epi {tc} {ta} {c} {arrow-ca} {arrow-ca} {h} refl = refl
|
|
|
132 epi {ta} {tb} {c} {arrow-ab} {arrow-ab} {h} refl = refl
|
|
|
133 epi {tb} {td} {c} {arrow-bd} {arrow-bd} {h} refl = refl
|
|
|
134 epi {tc} {tb} {c} {arrow-cb} {arrow-cb} {h} refl = refl
|
|
|
135 epi {ta} {td} {c} {arrow-ad} {arrow-ad} {h} refl = refl
|
|
|
136 epi {tc} {td} {c} {arrow-cd} {arrow-cd} {h} refl = refl
|
|
|
137
|
|
|
138 monic : {a b c : FourObject } {g₁ g₂ : Hom FourCat b c } { h : Hom FourCat a b }
|
|
|
139 → FourCat [ g₁ o h ] ≡ FourCat [ g₂ o h ] → g₁ ≡ g₂
|
|
|
140 monic {a} {ta} {ta} {id-ta} {id-ta} {h} refl = refl
|
|
|
141 monic {a} {tb} {tb} {id-tb} {id-tb} {h} refl = refl
|
|
|
142 monic {a} {tc} {tc} {id-tc} {id-tc} {h} refl = refl
|
|
|
143 monic {a} {td} {td} {id-td} {id-td} {h} refl = refl
|
|
|
144 monic {a} {tc} {ta} {arrow-ca} {arrow-ca} {h} refl = refl
|
|
|
145 monic {a} {ta} {tb} {arrow-ab} {arrow-ab} {h} refl = refl
|
|
|
146 monic {a} {tb} {td} {arrow-bd} {arrow-bd} {h} refl = refl
|
|
|
147 monic {a} {tc} {tb} {arrow-cb} {arrow-cb} {h} refl = refl
|
|
|
148 monic {a} {ta} {td} {arrow-ad} {arrow-ad} {h} refl = refl
|
|
|
149 monic {a} {tc} {td} {arrow-cd} {arrow-cd} {h} refl = refl
|
|
|
150
|
|
|
151 open import cat-utility
|
|
|
152 open import Relation.Nullary
|
|
|
153 open import Data.Empty
|
|
|
154
|
|
|
155 record Rev {a b : FourObject } (f : Hom FourCat a b ) : Set where
|
|
|
156 field
|
|
|
157 rev : Hom FourCat b a
|
|
|
158 eq : FourCat [ f o rev ] ≡ id1 FourCat b
|
|
|
159
|
|
|
160 not-rev : ¬ ( {a b : FourObject } → (f : Hom FourCat a b ) → Rev f )
|
|
|
161 not-rev r = ⊥-elim ( lemma1 arrow-ab (Rev.rev (r arrow-ab)) (Rev.eq (r arrow-ab)) )
|
|
|
162 where
|
|
|
163 lemma1 : (f : Hom FourCat ta tb ) → (e₁ : Hom FourCat tb ta )
|
|
|
164 → ( FourCat [ f o e₁ ] ≡ id1 FourCat tb ) → ⊥
|
|
|
165 lemma1 _ () eq
|
