open import Category -- https://github.com/konn/category-agda
open import Level
--open import Category.HomReasoning
open import HomReasoning
open import cat-utility
open import Category.Cat

module code-data { c₁ c₂ ℓ : Level} { A : Category c₁ c₂ ℓ } where

record DataObj : Set (c₁ ⊔ c₂ ⊔ ℓ)  where
   field
      dom : Obj A
      codom : Obj A
      code : Hom A dom codom
      rev-code : Hom A codom dom
      id-left  :  A [ A [ code  o rev-code ]  ≈  id1 A codom ]

open DataObj

record isDataHom (a : DataObj ) (b : DataObj ) : Set (c₁ ⊔ c₂ ⊔ ℓ) where
   field
      history : Hom A (codom a) (dom b)
   data-dom = a
   data-codom = b

open isDataHom

DataHom : (a : DataObj ) (b : DataObj ) → Set (c₁ ⊔ c₂ ⊔ ℓ)
DataHom = λ a b →  isDataHom a b

DataId : { a : DataObj } → DataHom a a
DataId {a} = record {
      history = rev-code a
   }

_∙_ :  {a b c : DataObj } → DataHom b c → DataHom a b → DataHom a c
_∙_ {a} {b} {c} g f = record { history = A [ history g o A [ code b o history f ] ] }

_≗_ : {a : DataObj } {b : DataObj } (f g : DataHom a b ) → Set ℓ 
_≗_ {a} {b} f g = A [  A [ code b o history f ]  ≈  A [ code b o history g ]  ]

open import Relation.Binary.Core

iDataCategory : IsCategory DataObj DataHom _≗_ _∙_  DataId 
iDataCategory  = record  { isEquivalence =  isEquivalence 
                    ; 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} -> associative a b c d f g h
                    }
     where
         open ≈-Reasoning (A) 
         o-resp :  {A B C : DataObj} {f g : DataHom A B} {h i : DataHom B C} → f ≗ g → h ≗ i → (h ∙ f) ≗ (i ∙ g)
         o-resp {a} {b} {c} {f} {g} {h} {i} f≗g h≗i =  begin
                code c o history (h ∙ f) 
           ≈⟨⟩
                code c o history h o code b o history f
           ≈⟨ cdr ( cdr ( f≗g ) ) ⟩
                code c o history h o code b o history g
           ≈⟨ assoc ⟩
                (code c o history h ) o code b o history g
           ≈⟨ car h≗i ⟩
                (code c o history i ) o code b o history g
           ≈⟨ sym assoc ⟩
                code c o history i o code b o history g
           ≈⟨⟩
                code c o history (i ∙ g)
           ∎ 
         associative : (a b c d : DataObj)  (f : DataHom c d) (g : DataHom b c) (h : DataHom a b) → (f ∙ (g ∙ h)) ≗ ((f ∙ g) ∙ h)
         associative a b c d f g h  = begin
               code d o history (f ∙ (g ∙ h))
           ≈⟨⟩
               code d o history f o code c o  history g  o code b o history h  
           ≈⟨ cdr (cdr assoc ) ⟩
               code d o history f o (code c o  history g)  o code b o history h  
           ≈⟨ cdr assoc ⟩
               code d o (history f o code c o history g) o code b o history h
           ≈⟨⟩
               code d o history ((f ∙ g) ∙ h) 
           ∎
         identityL : (a : DataObj) (b : DataObj) (f : DataHom a b) → (DataId ∙ f) ≗ f
         identityL a b f  = begin
              code b o history (DataId ∙ f) 
           ≈⟨⟩
               code b o ( rev-code b o  (code b o history f ))
           ≈⟨ assoc ⟩
               (code b o  rev-code b ) o  ( code b o history f )
           ≈⟨ car (id-left b )  ⟩
               id1 A (codom b) o  ( code b o history f )
           ≈⟨ idL ⟩
              code b o history f 
           ∎
         identityR : (a : DataObj) (b : DataObj) (f : DataHom a b) → (f ∙ DataId  ) ≗ f
         identityR a b f  = begin
               code b o history (f ∙ DataId) 
           ≈⟨⟩
               code b o ( history f  o ( code a   o rev-code a ) )
           ≈⟨ cdr (cdr (id-left a)) ⟩
               code b o ( history f  o id1 A (codom a) )
           ≈⟨ cdr idR ⟩
               code b o history f
           ∎
         isEquivalence : {a : DataObj } {b : DataObj } →
               IsEquivalence {_} {_} {DataHom a b } _≗_
         isEquivalence {C} {D} =      -- this is the same function as A's equivalence but has different types
           record { refl  = refl-hom
             ; sym   = sym
             ; trans = trans-hom
             } 
DataCategory : Category (c₁ ⊔ c₂ ⊔ ℓ) (c₁ ⊔ c₂ ⊔ ℓ) ℓ
DataCategory =
  record { Obj = DataObj
         ; Hom = DataHom
         ; _o_ = _∙_ 
         ; _≈_ = _≗_
         ; Id  =  DataId 
         ; isCategory = iDataCategory
          }



open Functor
open NTrans

F : Obj A -> Obj DataCategory  
F d  = record {
      dom  = d
      ; codom = d
      ; code  = id1 A d
      ; rev-code  = id1 A d
      ; id-left = idL
   }  where open ≈-Reasoning (A)  

U : Functor  DataCategory A
U = record {
      FObj = \d -> codom  d
    ; FMap = \f -> A [ code ( data-codom f ) o history f ] 
    ; isFunctor = record {
             ≈-cong   =  \{a} {b} {f} {g} -> ≈-cong-1 {a} {b} {f} {g}
             ; identity = \{a} -> identity-1 {a}
             ; distr    = \{a b c f g} -> distr-1 {a} {b} {c} {f} {g}
      }
 } where
    open ≈-Reasoning (A) 
    ≈-cong-1 :  {a : Obj DataCategory} {b : Obj DataCategory} {f g : Hom DataCategory a b} → DataCategory [ f ≈ g ] → 
         A [ A [ code (data-codom f) o history f ] ≈ A [ code (data-codom g) o history g ] ]
    ≈-cong-1 {a} {b} {f} {g}  f≈g =  begin
              code (data-codom f) o history f 
           ≈⟨⟩
              code b o history f 
           ≈⟨ f≈g ⟩
              code b o history g 
           ≈⟨⟩
              code (data-codom g) o history g 
           ∎
    identity-1 :  {a : Obj DataCategory} → A [ A [ code (data-codom (DataId {a})) o history (DataId {a}) ] ≈ id1 A (codom a) ]
    identity-1 {a} =   begin
              code (data-codom (DataId {a} )) o history (DataId  {a} )
           ≈⟨⟩
               code a o  rev-code a
           ≈⟨ id-left a ⟩
              id1 A (codom a)
           ∎
    distr-1 :  {a b c : Obj DataCategory} {f : Hom DataCategory a b} {g : Hom DataCategory b c} → 
             A [ A [ code (data-codom ( g ∙ f )) o history ( g ∙ f ) ] ≈
                A [ A [ code (data-codom g) o history g ] o A [ code (data-codom f) o history f ] ] ]
    distr-1 {a} {b} {c} {f} {g} =  begin
               code (data-codom (g ∙ f )) o history ( g ∙ f ) 
           ≈⟨⟩
                code c o history g o  code b o history f
           ≈⟨ assoc ⟩
                (code c o history g ) o  code b o history f
           ≈⟨⟩
               ( code (data-codom g) o history g ) o ( code (data-codom f) o history f )
           ∎

eta-map :   (a : Obj A) → Hom A a ( FObj U (F a) )
eta-map a = id1 A a


Lemma1 :  UniversalMapping A DataCategory U F eta-map
Lemma1 = record {
         _* =  solution ;
         isUniversalMapping = record {
                    universalMapping  = \{a} {b} {f} -> universalMapping {a} {b} {f} ;
                    uniquness = \{a} {b} {f} {g} -> uniqueness {a} {b} {f} {g}
              }
  } where
    open ≈-Reasoning (A) 
    solution :  {a : Obj A} {b : Obj DataCategory} → Hom A a (FObj U b) → Hom DataCategory (F a) b
    solution {a} {b} f = record { history = A [ rev-code b o f ]  }
    universalMapping :  {a : Obj A} {b : Obj DataCategory} {f : Hom A a (FObj U b)} → A [ A [ FMap U (solution {a} {b} f) o eta-map a ] ≈ f ]
    universalMapping {a} {b} {f} = begin
                FMap U (solution {a} {b} f) o eta-map a 
           ≈⟨⟩
               (code b o ( rev-code b  o f))  o id1 A a
           ≈⟨ idR  ⟩
               code b o ( rev-code b  o f)
           ≈⟨ assoc  ⟩
               (code b o  rev-code b  ) o f
           ≈⟨ car (id-left b) ⟩
               id1 A (codom b) o f
           ≈⟨ idL ⟩
                f
           ∎
    uniqueness :  {a : Obj A} {b : Obj DataCategory} {f : Hom A a (FObj U b)}
        {g : Hom DataCategory (F a) b} →
        A [ A [ FMap U g o eta-map a ] ≈ f ] →
        DataCategory [ solution f ≈ g ]
    uniqueness {a} {b} {f} {g} Uη≈f  =  begin
               code b o history (solution {a} {b} f)
           ≈⟨⟩
               code b o ( rev-code b o f)
           ≈⟨ sym ( cdr ( cdr  Uη≈f   )) ⟩
               code b o  rev-code b o ( code b o history g ) o id1 A (codom (F a))
           ≈⟨ assoc ⟩
               (code b o  rev-code b ) o ( code b o history g ) o id1 A (codom (F a))
           ≈⟨ car ( id-left b) ⟩
               id1 A (codom b ) o ( code b o history g ) o id1 A (codom (F a))
           ≈⟨ idL ⟩
               ( code b o history g ) o id1 A (codom (F a))
           ≈⟨ idR ⟩
               code b o history g
           ∎