module AgsyUnifier where

open import Relation.Binary.HeterogeneousEquality
open ≅-Reasoning
open import Function using (_∘_)

record Cat : Set₁ where
  infixr 7 _∙_
  field Obj  : Set
        Hom  : Obj → Obj → Set
        iden : ∀{X} → Hom X X
        _∙_ : ∀{X Y Z} → Hom Y Z → Hom X Y → Hom X Z
        idl  : ∀{X Y}{f : Hom X Y} → iden ∙ f ≅ f
        idr  : ∀{X Y}{f : Hom X Y} → f ∙ iden ≅ f
        ass  : ∀{W X Y Z}{f : Hom Y Z}{g : Hom X Y}{h : Hom W X} → 
               (f ∙ g) ∙ h ≅  f ∙ (g ∙ h)
               
record Iso (C : Cat){A B}(f : Cat.Hom C A B) : Set
  where
  constructor iso
  open Cat C
  field inv  : Hom B A
        rinv : f ∙ inv ≅ iden {B}
        linv : inv ∙ f ≅ iden {A}

comp-iso : (C : Cat){X Y Z : _}{f : Cat.Hom C Y Z}{g : Cat.Hom C X Y} →
            Iso C f → Iso C g → Iso C (Cat._∙_ C f g)
comp-iso C {f = f} {g} (iso inv law1 law2) (iso inv₁ law3 law4)
            = let open Cat C in 
            iso (inv₁ ∙ inv)
                (begin (f ∙ g) ∙ inv₁ ∙ inv
                       ≅⟨ ass ⟩
                       f ∙ g ∙ inv₁ ∙ inv
                       ≅⟨ cong (_∙_ f) (sym ass) ⟩
                       f ∙ (g ∙ inv₁) ∙ inv
                       ≅⟨ cong (λ x → f ∙ x ∙ inv) law3 ⟩
                       f ∙ iden ∙ inv
                       ≅⟨ cong (_∙_ f) idl ⟩
                       f ∙ inv
                       ≅⟨ law1 ⟩
                       iden ∎)
                (begin (inv₁ ∙ inv) ∙ f ∙ g
                       ≅⟨ ass ⟩
                       inv₁ ∙ inv ∙ f ∙ g
                       ≅⟨ cong (_∙_ inv₁) (sym ass) ⟩
                       inv₁ ∙ (inv ∙ f) ∙ g
                       ≅⟨ cong (λ x → inv₁ ∙ x ∙ g) law2 ⟩
                       inv₁ ∙ iden ∙ g
                       ≅⟨ cong (_∙_ inv₁) idl ⟩
                       inv₁ ∙ g
                       ≅⟨ law4 ⟩
                       iden ∎)


record Fun (C : Cat)(D : Cat) : Set where
  constructor functor
  open Cat
  field OMap  : Obj C → Obj D
        HMap  : ∀{X Y} → Hom C X Y → Hom D (OMap X) (OMap Y)
        fid   : ∀{X} → HMap (iden C {X}) ≅ iden D {OMap X}
        fcomp : ∀{X Y Z}{f : Hom C Y Z}{g : Hom C X Y} → 
                HMap (_∙_ C f g) ≅ _∙_ D (HMap f) (HMap g)


_○_ : (C : Cat)(D : Cat)(E : Cat) → 
      Fun D E → Fun C D → Fun C E
_○_ C D E F G = let open Cat
                    open Fun in record
                         { OMap = OMap F ∘ OMap G
                         ; HMap = λ {X Y} f → HMap F {OMap G X} {OMap G Y} (HMap G {X} {Y} f)
                         ; fid = λ {X} → begin
                                         {!!}
                                         ≅⟨ {!!} {- cong (HMap F) (fid G) -} ⟩
                                         {!!}
                                         ≅⟨ {!!} {- fid F -} ⟩
                                         {!!}
                                         ∎ 
                         ; fcomp = λ {X Y Z f g} → begin
                                                   {!!}
                                                   ≅⟨ {!!} {- cong (HMap F) (fcomp G) -} ⟩
                                                   {!!}
                                                   ≅⟨ {!!} {- fcomp F -} ⟩
                                                   {!!}
                                                   ∎
                         }