# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1537866374 -32400
# Node ID 5a3ca9509fbfa5e8b7c056b720a6190d4311eb42
# Parent  06a7831cf6cea730d491377dc966862a6424ed57
add epi

diff -r 06a7831cf6ce -r 5a3ca9509fbf epi.agda
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/epi.agda	Tue Sep 25 18:06:14 2018 +0900
@@ -0,0 +1,165 @@
+open import Category -- https://github.com/konn/category-agda
+open import Level
+
+module epi where
+
+open import Relation.Binary.Core
+
+data  FourObject   : Set where
+   ta : FourObject
+   tb : FourObject
+   tc : FourObject
+   td : FourObject
+
+data FourHom  : FourObject → FourObject → Set  where
+   id-ta :    FourHom ta ta
+   id-tb :    FourHom tb tb
+   id-tc :    FourHom tc tc
+   id-td :    FourHom td td
+   arrow-ca :  FourHom tc ta
+   arrow-ab :  FourHom ta tb
+   arrow-bd :  FourHom tb td
+   arrow-cb :  FourHom tc tb
+   arrow-ad :  FourHom ta td
+   arrow-cd :  FourHom tc td
+
+
+_×_ :  {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
+
+FourId :   (a : FourObject  ) →  (FourHom  a a )
+FourId ta = id-ta 
+FourId tb = id-tb 
+FourId tc = id-tc 
+FourId td = id-td 
+
+open import Relation.Binary.PropositionalEquality 
+
+FourCat :  Category   zero zero zero
+FourCat    = record {
+    Obj  = FourObject ;
+    Hom = λ a b →   FourHom a b  ;
+    _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}
+       }
+   }  where
+        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
+        identityL  {td} {td} {id-td} = refl
+        identityL  {tc} {ta} {arrow-ca} = refl
+        identityL  {ta} {tb} {arrow-ab} = refl
+        identityL  {tb} {td} {arrow-bd} = refl
+        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  {ta} {ta} {id-ta} = refl
+        identityR  {tb} {tb} {id-tb} = refl
+        identityR  {tc} {tc} {id-tc} = refl
+        identityR  {td} {td} {id-td} = refl
+        identityR  {tc} {ta} {arrow-ca} = refl
+        identityR  {ta} {tb} {arrow-ab} = refl
+        identityR  {tb} {td} {arrow-bd} = refl
+        identityR  {tc} {tb} {arrow-cb} = refl
+        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 )
+        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
+
+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
+
+open import cat-utility
+open import Relation.Nullary
+open import Data.Empty
+
+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
+
+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))  )
+  where
+     lemma1 :  (f : Hom FourCat ta tb )  →  (e₁ : Hom FourCat tb ta )
+          → ( FourCat  [ f o e₁ ]  ≡ id1 FourCat tb )  →  ⊥
+     lemma1 _ () eq