{-# OPTIONS --type-in-type #-}

-- we abuse terminology where our categories are always ordered categories,
-- poset enriched categories

module Base where

open import Relation.Binary.PropositionalEquality hiding (J) public
open ≡-Reasoning public
open import Data.Product public
open import Data.Unit public

infixr  _◇_

-- sequential (reverse) agda composition
_◇_ : {A B C : Set} → (A → B) → (B → C) → A → C
_◇_ f g a = g (f a)

-- the object type is a part of the type signature, instead of being contained
-- within the record
record ParamCategory (c : Set) : Set where
  infixr  _▷_
  infix  _≤_
  field
    hom : (X Y : c) → Set
    id : (X : c) → hom X X
    _▷_ : {X Y Z : c} → hom X Y → hom Y Z → hom X Z
    _≤_ : {X Y : c} → hom X Y → hom X Y → Set
    ▷lunit : {X Y : c} → {f : hom X Y} → id X ▷ f ≡ f
    ▷runit : {X Y : c} → {f : hom X Y} → f ≡ f ▷ id Y
    ▷assoc : {X Y Z W : c} → {f : hom X Y} → {g : hom Y Z} → {h : hom Z W}
      → (f ▷ g) ▷ h ≡ f ▷ (g ▷ h)

    ≤refl : {X Y : c} → {f : hom X Y}  → f ≤ f
    ≤trans : {X Y : c} → {f g h : hom X Y} → f ≤ g → g ≤ h → f ≤ h
    ≤antisym : {X Y : c} → {f g : hom X Y} → f ≤ g → g ≤ f → f ≡ g
    
    ▷monot≤ : {X Y Z : c} → {f f' : hom X Y} → {g g' : hom Y Z}
           → f ≤ f' → g ≤ g' → (f ▷ g) ≤ (f' ▷ g')

record Category : Set where
  field
    obj : Set
    PC : ParamCategory obj
  open ParamCategory PC public

-- here the object component of the functor is included in the type signature
-- which is useful for defining MonoidalProduct, I and J
record ParamPrefunctor {c d : Set}
                       (ℂ : ParamCategory c) (𝔻 : ParamCategory d)
                       (F₀ : c → d) : Set where
  private
    module ℂ = ParamCategory ℂ
    module 𝔻 = ParamCategory 𝔻
  field
    F₁ : ∀ {X Y} → ℂ.hom X Y → 𝔻.hom (F₀ X) (F₀ Y)
    preserveOrder : {X Y : c} {f g : ℂ.hom X Y}
                    → f ℂ.≤ g → (F₁ f) 𝔻.≤ (F₁ g)

record IsParamLaxFunctor {c d : Set}
       {ℂ : ParamCategory c} {𝔻 : ParamCategory d} {F₀ : c → d}
       (L : ParamPrefunctor ℂ 𝔻 F₀) : Set where
  private
    module ℂ = ParamCategory ℂ 
    module 𝔻 = ParamCategory 𝔻 
  open ParamPrefunctor L
  field
    laxIdentity : ∀ {X} → (𝔻.id (F₀ X)) 𝔻.≤ (F₁ (ℂ.id X))
    laxComposition : ∀ {X Y Z} {f : ℂ.hom X Y} {g : ℂ.hom Y Z}
                     → (F₁ f) 𝔻.▷ (F₁ g) 𝔻.≤ F₁ (f ℂ.▷ g)

record IsParamFunctor {c d : Set}
       {ℂ : ParamCategory c} {𝔻 : ParamCategory d} {F₀ : c → d}
       (L : ParamPrefunctor ℂ 𝔻 F₀) : Set where
  private
    module ℂ = ParamCategory ℂ 
    module 𝔻 = ParamCategory 𝔻
  open ParamPrefunctor L
  field
    strictIdentity : ∀ {X} → F₁ (ℂ.id X) ≡ 𝔻.id (F₀ X)
    strictComposition : ∀ {X Y Z} {f : ℂ.hom X Y} {g : ℂ.hom Y Z}
                     → F₁ (f ℂ.▷ g) ≡ (F₁ f) 𝔻.▷ (F₁ g)

record ParamLaxFunctor {c d : Set}
       (ℂ : ParamCategory c) (𝔻 : ParamCategory d) (F₀ : c → d) : Set where
  field
    prefunctor : ParamPrefunctor ℂ 𝔻 F₀
    isParamLaxFunctor : IsParamLaxFunctor prefunctor
  open ParamPrefunctor prefunctor public
  open IsParamLaxFunctor isParamLaxFunctor public

record ParamFunctor {c d : Set}
       (ℂ : ParamCategory c) (𝔻 : ParamCategory d) (F₀ : c → d) : Set where
  field
    prefunctor : ParamPrefunctor ℂ 𝔻 F₀
    isParamFunctor : IsParamFunctor prefunctor
  open ParamPrefunctor prefunctor public
  open IsParamFunctor isParamFunctor public

record Functor (ℂ 𝔻 : Category) : Set where
  private
    module ℂ = Category ℂ
    module 𝔻 = Category 𝔻
  field
    F₀ : ℂ.obj → 𝔻.obj
  field
    PF : ParamFunctor ℂ.PC 𝔻.PC F₀
  open ParamFunctor PF public

-- it's comfortable to see in the type signature what the
-- category's objects are
ParamProduct : {c d : Set} (ℂ : ParamCategory c) (𝔻 : ParamCategory d)
             → ParamCategory (c × d)
ParamProduct ℂ 𝔻 = let module ℂ = ParamCategory ℂ
                       module 𝔻 = ParamCategory 𝔻
      in record { hom = λ { (A , B) (U , V) → (ℂ.hom A U) × (𝔻.hom B V)}
                ; id = λ { (A , B) → ℂ.id A , 𝔻.id B }
                ; _▷_ =   λ { (f0 , f1) (g0 , g1) → f0 ℂ.▷ g0 , f1 𝔻.▷ g1 }
                ; _≤_ =  λ { (f0 , f1) (g0 , g1) → (f0 ℂ.≤ g0) × (f1 𝔻.≤ g1) }
                ; ▷lunit = cong₂ _,_ ℂ.▷lunit 𝔻.▷lunit
                ; ▷runit = cong₂ _,_ ℂ.▷runit 𝔻.▷runit
                ; ▷assoc = cong₂ _,_ ℂ.▷assoc 𝔻.▷assoc
                ; ≤refl =  ℂ.≤refl , 𝔻.≤refl
                ; ≤trans = λ { (fg0 , fg1) (gh0 , gh1)
                           → ℂ.≤trans fg0 gh0 , 𝔻.≤trans fg1 gh1 }
                ; ≤antisym = λ (fg0 , fg1) (gf0 , gf1) →
                             cong₂ _,_ (ℂ.≤antisym fg0 gf0) (𝔻.≤antisym fg1 gf1)
                ; ▷monot≤ = λ (ff'0 , ff'1) (gg'0 , gg'1)
                           → (ℂ.▷monot≤ ff'0 gg'0) , 𝔻.▷monot≤ ff'1 gg'1
                }

𝟙 : ParamCategory ⊤
𝟙 = record { hom = λ {tt tt → ⊤}
           ; id = λ {tt → tt}
           ; _▷_ = λ {tt tt → tt}
           ; _≤_ = λ {tt tt → ⊤}
           ; ▷lunit = refl
           ; ▷runit = refl
           ; ▷assoc = refl
           ; ≤refl = tt
           ; ≤trans = λ {tt tt → tt}
           ; ≤antisym = λ {tt tt → refl}
           ; ▷monot≤ = λ {tt tt → tt}
           }