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