Mercurial > hg > Members > kono > Proof > category

comparison epi.agda @ 776:5a3ca9509fbf

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
add epi
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Tue, 25 Sep 2018 18:06:14 +0900
parents
children 5160b431f1de
comparison
equal deleted inserted replaced
775:06a7831cf6ce 776:5a3ca9509fbf
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