|
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
|
|
777
|
26 --
|
|
|
27 -- epi and monic but does not have inverted arrow
|
|
|
28 --
|
|
|
29 -- +--------------------------+
|
|
|
30 -- | |
|
|
|
31 -- c-----------------+ |
|
|
|
32 -- | ↓ ↓
|
|
|
33 -- + ----→ a ----→ b ----→ d
|
|
|
34 -- | ↑
|
|
|
35 -- +-----------------+
|
|
|
36 --
|
|
776
|
37
|
|
777
|
38
|
|
|
39 _・_ : {a b c : FourObject } → FourHom b c → FourHom a b → FourHom a c
|
|
|
40 _・_ {x} {ta} {ta} id-ta y = y
|
|
|
41 _・_ {x} {tb} {tb} id-tb y = y
|
|
|
42 _・_ {x} {tc} {tc} id-tc y = y
|
|
|
43 _・_ {x} {td} {td} id-td y = y
|
|
|
44 _・_ {ta} {ta} {x} y id-ta = y
|
|
|
45 _・_ {tb} {tb} {x} y id-tb = y
|
|
|
46 _・_ {tc} {tc} {x} y id-tc = y
|
|
|
47 _・_ {td} {td} {x} y id-td = y
|
|
|
48 _・_ {tc} {ta} {tb} arrow-ab arrow-ca = arrow-cb
|
|
|
49 _・_ {ta} {tb} {td} arrow-bd arrow-ab = arrow-ad
|
|
|
50 _・_ {tc} {tb} {td} arrow-bd arrow-cb = arrow-cd
|
|
|
51 _・_ {tc} {ta} {td} arrow-ad arrow-ca = arrow-cd
|
|
|
52 _・_ {tc} {ta} {tc} () arrow-ca
|
|
|
53 _・_ {ta} {tb} {ta} () arrow-ab
|
|
|
54 _・_ {tc} {tb} {ta} () arrow-cb
|
|
|
55 _・_ {ta} {tb} {tc} () arrow-ab
|
|
|
56 _・_ {tc} {tb} {tc} () arrow-cb
|
|
|
57 _・_ {tb} {td} {ta} () arrow-bd
|
|
|
58 _・_ {ta} {td} {ta} () arrow-ad
|
|
|
59 _・_ {tc} {td} {ta} () arrow-cd
|
|
|
60 _・_ {tb} {td} {tb} () arrow-bd
|
|
|
61 _・_ {ta} {td} {tb} () arrow-ad
|
|
|
62 _・_ {tc} {td} {tb} () arrow-cd
|
|
|
63 _・_ {tb} {td} {tc} () arrow-bd
|
|
|
64 _・_ {ta} {td} {tc} () arrow-ad
|
|
|
65 _・_ {tc} {td} {tc} () arrow-cd
|
|
776
|
66
|
|
|
67 open FourHom
|
|
|
68
|
|
|
69
|
|
777
|
70 assoc-・ : {a b c d : FourObject }
|
|
|
71 (f : FourHom c d ) → (g : FourHom b c ) → (h : FourHom a b ) →
|
|
|
72 ( f ・ (g ・ h)) ≡ ((f ・ g) ・ h )
|
|
|
73 assoc-・ id-ta y z = refl
|
|
|
74 assoc-・ id-tb y z = refl
|
|
|
75 assoc-・ id-tc y z = refl
|
|
|
76 assoc-・ id-td y z = refl
|
|
|
77 assoc-・ arrow-ca id-tc z = refl
|
|
|
78 assoc-・ arrow-ab id-ta z = refl
|
|
|
79 assoc-・ arrow-ab arrow-ca id-tc = refl
|
|
|
80 assoc-・ arrow-bd id-tb z = refl
|
|
|
81 assoc-・ arrow-bd arrow-ab id-ta = refl
|
|
|
82 assoc-・ arrow-bd arrow-ab arrow-ca = refl
|
|
|
83 assoc-・ arrow-bd arrow-cb id-tc = refl
|
|
|
84 assoc-・ arrow-cb id-tc z = refl
|
|
|
85 assoc-・ arrow-ad id-ta z = refl
|
|
|
86 assoc-・ arrow-ad arrow-ca id-tc = refl
|
|
|
87 assoc-・ arrow-cd id-tc id-tc = refl
|
|
776
|
88
|
|
|
89 FourId : (a : FourObject ) → (FourHom a a )
|
|
|
90 FourId ta = id-ta
|
|
|
91 FourId tb = id-tb
|
|
|
92 FourId tc = id-tc
|
|
|
93 FourId td = id-td
|
|
|
94
|
|
|
95 open import Relation.Binary.PropositionalEquality
|
|
|
96
|
|
|
97 FourCat : Category zero zero zero
|
|
|
98 FourCat = record {
|
|
|
99 Obj = FourObject ;
|
|
|
100 Hom = λ a b → FourHom a b ;
|
|
777
|
101 _o_ = λ{a} {b} {c} x y → _・_ x y ;
|
|
776
|
102 _≈_ = λ x y → x ≡ y ;
|
|
|
103 Id = λ{a} → FourId a ;
|
|
|
104 isCategory = record {
|
|
|
105 isEquivalence = record {refl = refl ; trans = trans ; sym = sym } ; identityL = λ{a b f} → identityL {a} {b} {f} ;
|
|
|
106 identityR = λ{a b f} → identityR {a} {b} {f} ;
|
|
|
107 o-resp-≈ = λ{a b c f g h i} → o-resp-≈ {a} {b} {c} {f} {g} {h} {i} ;
|
|
777
|
108 associative = λ{a b c d f g h } → assoc-・ f g h
|
|
776
|
109 }
|
|
|
110 } where
|
|
777
|
111 identityL : {A B : FourObject } {f : ( FourHom A B) } → ((FourId B) ・ f) ≡ f
|
|
776
|
112 identityL {ta} {ta} {id-ta} = refl
|
|
|
113 identityL {tb} {tb} {id-tb} = refl
|
|
|
114 identityL {tc} {tc} {id-tc} = refl
|
|
|
115 identityL {td} {td} {id-td} = refl
|
|
|
116 identityL {tc} {ta} {arrow-ca} = refl
|
|
|
117 identityL {ta} {tb} {arrow-ab} = refl
|
|
|
118 identityL {tb} {td} {arrow-bd} = refl
|
|
|
119 identityL {tc} {tb} {arrow-cb} = refl
|
|
|
120 identityL {ta} {td} {arrow-ad} = refl
|
|
|
121 identityL {tc} {td} {arrow-cd} = refl
|
|
777
|
122 identityR : {A B : FourObject } {f : ( FourHom A B) } → ( f ・ FourId A ) ≡ f
|
|
776
|
123 identityR {ta} {ta} {id-ta} = refl
|
|
|
124 identityR {tb} {tb} {id-tb} = refl
|
|
|
125 identityR {tc} {tc} {id-tc} = refl
|
|
|
126 identityR {td} {td} {id-td} = refl
|
|
|
127 identityR {tc} {ta} {arrow-ca} = refl
|
|
|
128 identityR {ta} {tb} {arrow-ab} = refl
|
|
|
129 identityR {tb} {td} {arrow-bd} = refl
|
|
|
130 identityR {tc} {tb} {arrow-cb} = refl
|
|
|
131 identityR {ta} {td} {arrow-ad} = refl
|
|
|
132 identityR {tc} {td} {arrow-cd} = refl
|
|
|
133 o-resp-≈ : {A B C : FourObject } {f g : ( FourHom A B)} {h i : ( FourHom B C)} →
|
|
777
|
134 f ≡ g → h ≡ i → ( h ・ f ) ≡ ( i ・ g )
|
|
776
|
135 o-resp-≈ {a} {b} {c} {f} {x} {h} {y} refl refl = refl
|
|
|
136
|
|
777
|
137 epi : {a b c : FourObject } (f₁ f₂ : Hom FourCat a b ) ( h : Hom FourCat b c )
|
|
|
138 → h ・ f₁ ≡ h ・ f₂ → f₁ ≡ f₂
|
|
|
139 epi id-ta id-ta _ refl = refl
|
|
|
140 epi id-tb id-tb _ refl = refl
|
|
|
141 epi id-tc id-tc _ refl = refl
|
|
|
142 epi id-td id-td _ refl = refl
|
|
|
143 epi arrow-ca arrow-ca _ refl = refl
|
|
|
144 epi arrow-ab arrow-ab _ refl = refl
|
|
|
145 epi arrow-bd arrow-bd _ refl = refl
|
|
|
146 epi arrow-cb arrow-cb _ refl = refl
|
|
|
147 epi arrow-ad arrow-ad _ refl = refl
|
|
|
148 epi arrow-cd arrow-cd _ refl = refl
|
|
776
|
149
|
|
777
|
150 monic : {a b c : FourObject } (g₁ g₂ : Hom FourCat b c ) ( h : Hom FourCat a b )
|
|
|
151 → g₁ ・ h ≡ g₂ ・ h → g₁ ≡ g₂
|
|
|
152 monic id-ta id-ta _ refl = refl
|
|
|
153 monic id-tb id-tb _ refl = refl
|
|
|
154 monic id-tc id-tc _ refl = refl
|
|
|
155 monic id-td id-td _ refl = refl
|
|
|
156 monic arrow-ca arrow-ca _ refl = refl
|
|
|
157 monic arrow-ab arrow-ab _ refl = refl
|
|
|
158 monic arrow-bd arrow-bd _ refl = refl
|
|
|
159 monic arrow-cb arrow-cb _ refl = refl
|
|
|
160 monic arrow-ad arrow-ad _ refl = refl
|
|
|
161 monic arrow-cd arrow-cd _ refl = refl
|
|
776
|
162
|
|
|
163 open import cat-utility
|
|
|
164 open import Relation.Nullary
|
|
|
165 open import Data.Empty
|
|
|
166
|
|
|
167 record Rev {a b : FourObject } (f : Hom FourCat a b ) : Set where
|
|
|
168 field
|
|
|
169 rev : Hom FourCat b a
|
|
777
|
170 eq : f ・ rev ≡ id1 FourCat b
|
|
776
|
171
|
|
|
172 not-rev : ¬ ( {a b : FourObject } → (f : Hom FourCat a b ) → Rev f )
|
|
777
|
173 not-rev r = lemma1 arrow-ab (Rev.rev (r arrow-ab)) (Rev.eq (r arrow-ab))
|
|
776
|
174 where
|
|
|
175 lemma1 : (f : Hom FourCat ta tb ) → (e₁ : Hom FourCat tb ta )
|
|
777
|
176 → ( f ・ e₁ ≡ id1 FourCat tb ) → ⊥
|
|
776
|
177 lemma1 _ () eq
|
