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