# HG changeset patch # User Shinji KONO # Date 1537923602 -32400 # Node ID 5160b431f1de72a532d662f2b0adce7732874016 # Parent 5a3ca9509fbfa5e8b7c056b720a6190d4311eb42 fix diff -r 5a3ca9509fbf -r 5160b431f1de epi.agda --- a/epi.agda Tue Sep 25 18:06:14 2018 +0900 +++ b/epi.agda Wed Sep 26 10:00:02 2018 +0900 @@ -23,56 +23,68 @@ arrow-ad : FourHom ta td arrow-cd : FourHom tc td +-- +-- epi and monic but does not have inverted arrow +-- +-- +--------------------------+ +-- | | +-- c-----------------+ | +-- | ↓ ↓ +-- + ----→ a ----→ b ----→ d +-- | ↑ +-- +-----------------+ +-- -_×_ : {a b c : FourObject } → FourHom b c → FourHom a b → FourHom a c -_×_ {x} {ta} {ta} id-ta y = y -_×_ {x} {tb} {tb} id-tb y = y -_×_ {x} {tc} {tc} id-tc y = y -_×_ {x} {td} {td} id-td y = y -_×_ {ta} {ta} {x} y id-ta = y -_×_ {tb} {tb} {x} y id-tb = y -_×_ {tc} {tc} {x} y id-tc = y -_×_ {td} {td} {x} y id-td = y -_×_ {tc} {ta} {tb} arrow-ab arrow-ca = arrow-cb -_×_ {ta} {tb} {td} arrow-bd arrow-ab = arrow-ad -_×_ {tc} {tb} {td} arrow-bd arrow-cb = arrow-cd -_×_ {tc} {ta} {td} arrow-ad arrow-ca = arrow-cd -_×_ {tc} {ta} {tc} () arrow-ca -_×_ {ta} {tb} {ta} () arrow-ab -_×_ {tc} {tb} {ta} () arrow-cb -_×_ {ta} {tb} {tc} () arrow-ab -_×_ {tc} {tb} {tc} () arrow-cb -_×_ {tb} {td} {ta} () arrow-bd -_×_ {ta} {td} {ta} () arrow-ad -_×_ {tc} {td} {ta} () arrow-cd -_×_ {tb} {td} {tb} () arrow-bd -_×_ {ta} {td} {tb} () arrow-ad -_×_ {tc} {td} {tb} () arrow-cd -_×_ {tb} {td} {tc} () arrow-bd -_×_ {ta} {td} {tc} () arrow-ad -_×_ {tc} {td} {tc} () arrow-cd + +_・_ : {a b c : FourObject } → FourHom b c → FourHom a b → FourHom a c +_・_ {x} {ta} {ta} id-ta y = y +_・_ {x} {tb} {tb} id-tb y = y +_・_ {x} {tc} {tc} id-tc y = y +_・_ {x} {td} {td} id-td y = y +_・_ {ta} {ta} {x} y id-ta = y +_・_ {tb} {tb} {x} y id-tb = y +_・_ {tc} {tc} {x} y id-tc = y +_・_ {td} {td} {x} y id-td = y +_・_ {tc} {ta} {tb} arrow-ab arrow-ca = arrow-cb +_・_ {ta} {tb} {td} arrow-bd arrow-ab = arrow-ad +_・_ {tc} {tb} {td} arrow-bd arrow-cb = arrow-cd +_・_ {tc} {ta} {td} arrow-ad arrow-ca = arrow-cd +_・_ {tc} {ta} {tc} () arrow-ca +_・_ {ta} {tb} {ta} () arrow-ab +_・_ {tc} {tb} {ta} () arrow-cb +_・_ {ta} {tb} {tc} () arrow-ab +_・_ {tc} {tb} {tc} () arrow-cb +_・_ {tb} {td} {ta} () arrow-bd +_・_ {ta} {td} {ta} () arrow-ad +_・_ {tc} {td} {ta} () arrow-cd +_・_ {tb} {td} {tb} () arrow-bd +_・_ {ta} {td} {tb} () arrow-ad +_・_ {tc} {td} {tb} () arrow-cd +_・_ {tb} {td} {tc} () arrow-bd +_・_ {ta} {td} {tc} () arrow-ad +_・_ {tc} {td} {tc} () arrow-cd open FourHom -assoc-× : {a b c d : FourObject } - {f : (FourHom c d )} → {g : (FourHom b c )} → {h : (FourHom a b )} → - ( f × (g × h)) ≡ ((f × g) × h ) -assoc-× {_} {_} {_} {_} {id-ta} {y} {z} = refl -assoc-× {_} {_} {_} {_} {id-tb} {y} {z} = refl -assoc-× {_} {_} {_} {_} {id-tc} {y} {z} = refl -assoc-× {_} {_} {_} {_} {id-td} {y} {z} = refl -assoc-× {_} {_} {_} {_} {arrow-ca} {id-tc} {z} = refl -assoc-× {_} {_} {_} {_} {arrow-ab} {id-ta} {z} = refl -assoc-× {_} {_} {_} {_} {arrow-ab} {arrow-ca} {id-tc} = refl -assoc-× {_} {_} {_} {_} {arrow-bd} {id-tb} {z} = refl -assoc-× {_} {_} {_} {_} {arrow-bd} {arrow-ab} {id-ta} = refl -assoc-× {_} {_} {_} {_} {arrow-bd} {arrow-ab} {arrow-ca} = refl -assoc-× {_} {_} {_} {_} {arrow-bd} {arrow-cb} {id-tc} = refl -assoc-× {_} {_} {_} {_} {arrow-cb} {id-tc} {z} = refl -assoc-× {_} {_} {_} {_} {arrow-ad} {id-ta} {z} = refl -assoc-× {_} {_} {_} {_} {arrow-ad} {arrow-ca} {id-tc} = refl -assoc-× {_} {_} {_} {_} {arrow-cd} {id-tc} {id-tc} = refl +assoc-・ : {a b c d : FourObject } + (f : FourHom c d ) → (g : FourHom b c ) → (h : FourHom a b ) → + ( f ・ (g ・ h)) ≡ ((f ・ g) ・ h ) +assoc-・ id-ta y z = refl +assoc-・ id-tb y z = refl +assoc-・ id-tc y z = refl +assoc-・ id-td y z = refl +assoc-・ arrow-ca id-tc z = refl +assoc-・ arrow-ab id-ta z = refl +assoc-・ arrow-ab arrow-ca id-tc = refl +assoc-・ arrow-bd id-tb z = refl +assoc-・ arrow-bd arrow-ab id-ta = refl +assoc-・ arrow-bd arrow-ab arrow-ca = refl +assoc-・ arrow-bd arrow-cb id-tc = refl +assoc-・ arrow-cb id-tc z = refl +assoc-・ arrow-ad id-ta z = refl +assoc-・ arrow-ad arrow-ca id-tc = refl +assoc-・ arrow-cd id-tc id-tc = refl FourId : (a : FourObject ) → (FourHom a a ) FourId ta = id-ta @@ -86,17 +98,17 @@ FourCat = record { Obj = FourObject ; Hom = λ a b → FourHom a b ; - _o_ = λ{a} {b} {c} x y → _×_ x y ; + _o_ = λ{a} {b} {c} x y → _・_ x y ; _≈_ = λ x y → x ≡ y ; Id = λ{a} → FourId a ; isCategory = record { isEquivalence = record {refl = refl ; trans = trans ; sym = sym } ; identityL = λ{a b f} → identityL {a} {b} {f} ; identityR = λ{a b f} → identityR {a} {b} {f} ; o-resp-≈ = λ{a b c f g h i} → o-resp-≈ {a} {b} {c} {f} {g} {h} {i} ; - associative = λ{a b c d f g h } → assoc-× {a} {b} {c} {d} {f} {g} {h} + associative = λ{a b c d f g h } → assoc-・ f g h } } where - identityL : {A B : FourObject } {f : ( FourHom A B) } → ((FourId B) × f) ≡ f + identityL : {A B : FourObject } {f : ( FourHom A B) } → ((FourId B) ・ f) ≡ f identityL {ta} {ta} {id-ta} = refl identityL {tb} {tb} {id-tb} = refl identityL {tc} {tc} {id-tc} = refl @@ -107,7 +119,7 @@ identityL {tc} {tb} {arrow-cb} = refl identityL {ta} {td} {arrow-ad} = refl identityL {tc} {td} {arrow-cd} = refl - identityR : {A B : FourObject } {f : ( FourHom A B) } → ( f × FourId A ) ≡ f + identityR : {A B : FourObject } {f : ( FourHom A B) } → ( f ・ FourId A ) ≡ f identityR {ta} {ta} {id-ta} = refl identityR {tb} {tb} {id-tb} = refl identityR {tc} {tc} {id-tc} = refl @@ -119,34 +131,34 @@ identityR {ta} {td} {arrow-ad} = refl identityR {tc} {td} {arrow-cd} = refl o-resp-≈ : {A B C : FourObject } {f g : ( FourHom A B)} {h i : ( FourHom B C)} → - f ≡ g → h ≡ i → ( h × f ) ≡ ( i × g ) + f ≡ g → h ≡ i → ( h ・ f ) ≡ ( i ・ g ) o-resp-≈ {a} {b} {c} {f} {x} {h} {y} refl refl = refl -epi : {a b c : FourObject } {f₁ f₂ : Hom FourCat a b } { h : Hom FourCat b c } - → FourCat [ h o f₁ ] ≡ FourCat [ h o f₂ ] → f₁ ≡ f₂ -epi {ta} {ta} {c} {id-ta} {id-ta} {h} refl = refl -epi {tb} {tb} {c} {id-tb} {id-tb} {h} refl = refl -epi {tc} {tc} {c} {id-tc} {id-tc} {h} refl = refl -epi {td} {td} {c} {id-td} {id-td} {h} refl = refl -epi {tc} {ta} {c} {arrow-ca} {arrow-ca} {h} refl = refl -epi {ta} {tb} {c} {arrow-ab} {arrow-ab} {h} refl = refl -epi {tb} {td} {c} {arrow-bd} {arrow-bd} {h} refl = refl -epi {tc} {tb} {c} {arrow-cb} {arrow-cb} {h} refl = refl -epi {ta} {td} {c} {arrow-ad} {arrow-ad} {h} refl = refl -epi {tc} {td} {c} {arrow-cd} {arrow-cd} {h} refl = refl +epi : {a b c : FourObject } (f₁ f₂ : Hom FourCat a b ) ( h : Hom FourCat b c ) + → h ・ f₁ ≡ h ・ f₂ → f₁ ≡ f₂ +epi id-ta id-ta _ refl = refl +epi id-tb id-tb _ refl = refl +epi id-tc id-tc _ refl = refl +epi id-td id-td _ refl = refl +epi arrow-ca arrow-ca _ refl = refl +epi arrow-ab arrow-ab _ refl = refl +epi arrow-bd arrow-bd _ refl = refl +epi arrow-cb arrow-cb _ refl = refl +epi arrow-ad arrow-ad _ refl = refl +epi arrow-cd arrow-cd _ refl = refl -monic : {a b c : FourObject } {g₁ g₂ : Hom FourCat b c } { h : Hom FourCat a b } - → FourCat [ g₁ o h ] ≡ FourCat [ g₂ o h ] → g₁ ≡ g₂ -monic {a} {ta} {ta} {id-ta} {id-ta} {h} refl = refl -monic {a} {tb} {tb} {id-tb} {id-tb} {h} refl = refl -monic {a} {tc} {tc} {id-tc} {id-tc} {h} refl = refl -monic {a} {td} {td} {id-td} {id-td} {h} refl = refl -monic {a} {tc} {ta} {arrow-ca} {arrow-ca} {h} refl = refl -monic {a} {ta} {tb} {arrow-ab} {arrow-ab} {h} refl = refl -monic {a} {tb} {td} {arrow-bd} {arrow-bd} {h} refl = refl -monic {a} {tc} {tb} {arrow-cb} {arrow-cb} {h} refl = refl -monic {a} {ta} {td} {arrow-ad} {arrow-ad} {h} refl = refl -monic {a} {tc} {td} {arrow-cd} {arrow-cd} {h} refl = refl +monic : {a b c : FourObject } (g₁ g₂ : Hom FourCat b c ) ( h : Hom FourCat a b ) + → g₁ ・ h ≡ g₂ ・ h → g₁ ≡ g₂ +monic id-ta id-ta _ refl = refl +monic id-tb id-tb _ refl = refl +monic id-tc id-tc _ refl = refl +monic id-td id-td _ refl = refl +monic arrow-ca arrow-ca _ refl = refl +monic arrow-ab arrow-ab _ refl = refl +monic arrow-bd arrow-bd _ refl = refl +monic arrow-cb arrow-cb _ refl = refl +monic arrow-ad arrow-ad _ refl = refl +monic arrow-cd arrow-cd _ refl = refl open import cat-utility open import Relation.Nullary @@ -155,11 +167,11 @@ record Rev {a b : FourObject } (f : Hom FourCat a b ) : Set where field rev : Hom FourCat b a - eq : FourCat [ f o rev ] ≡ id1 FourCat b + eq : f ・ rev ≡ id1 FourCat b not-rev : ¬ ( {a b : FourObject } → (f : Hom FourCat a b ) → Rev f ) -not-rev r = ⊥-elim ( lemma1 arrow-ab (Rev.rev (r arrow-ab)) (Rev.eq (r arrow-ab)) ) +not-rev r = lemma1 arrow-ab (Rev.rev (r arrow-ab)) (Rev.eq (r arrow-ab)) where lemma1 : (f : Hom FourCat ta tb ) → (e₁ : Hom FourCat tb ta ) - → ( FourCat [ f o e₁ ] ≡ id1 FourCat tb ) → ⊥ + → ( f ・ e₁ ≡ id1 FourCat tb ) → ⊥ lemma1 _ () eq