Cat.agda

module Lib.Cat where

open import Agda.Primitive using (Level; lsuc; _⊔_)
open import Relation.Binary.PropositionalEquality public
open import Lib.Eq using (subst-dep₂)

private
  variable
    ℓ ℓʹ : Level

hom-set : (C : Set ℓ) → (ℓʹ : Level) → Set (ℓ ⊔ lsuc ℓʹ)
hom-set C ℓʹ = C → C → Set ℓʹ

hom-comp : {C : Set ℓ} → hom-set C ℓʹ → Set (ℓ ⊔ ℓʹ)
hom-comp {_} {_} {C} hom = {a b c : C} → hom b c → hom a b → hom a c

hom-comp-id : {C : Set ℓ} → (hom : hom-set C ℓʹ) → Set (ℓ ⊔ ℓʹ)
hom-comp-id {_} {_} {C} hom = (o : C) → hom o o

hom-comp-assoc : {C : Set ℓ} → (hom : hom-set C ℓʹ) → hom-comp hom → Set (ℓ ⊔ ℓʹ)
hom-comp-assoc {_} {_} {C} hom _∙_ = ∀ {a b c d : C} (f : hom c d) (g : hom b c) (h : hom a b) → (f ∙ g) ∙ h ≡ f ∙ (g ∙ h)

hom-comp-identˡ : {C : Set ℓ} → (hom : hom-set C ℓʹ) → hom-comp hom → hom-comp-id hom → Set (ℓ ⊔ ℓʹ)
hom-comp-identˡ {_} {_} {C} hom _∙_ id = ∀ (o : C) {oʹ : C} (f : hom oʹ o) → id o ∙ f ≡ f

hom-comp-identʳ : {C : Set ℓ} → (hom : hom-set C ℓʹ) → hom-comp hom → hom-comp-id hom → Set (ℓ ⊔ ℓʹ)
hom-comp-identʳ {_} {_} {C} hom _∙_ id = ∀ (o : C) {oʹ : C} (f : hom o oʹ) → f ∙ id o ≡ f

record Cat (C : Set ℓ) (ℓʹ : Level) : Set (ℓ ⊔ lsuc ℓʹ) where
  constructor NewCat
  field
    hom : hom-set C ℓʹ
    _∙_ : hom-comp hom
    id : hom-comp-id hom
    
    ∙-assoc : hom-comp-assoc hom _∙_
    ∙-identˡ : hom-comp-identˡ hom _∙_ id
    ∙-identʳ : hom-comp-identʳ hom _∙_ id  

private
  ≡-comp : ∀ {ℓ ℓʹ : Level} {C : Set ℓ} {hom homʹ : hom-set C ℓʹ} (hom-≡ : hom ≡ homʹ)
        → hom-comp hom → hom-comp homʹ → Set (ℓ ⊔ ℓʹ)
  ≡-comp {_} {_} {_} {_} {homʹ} hom-≡ comp compʹ = _≡_ {A = hom-comp homʹ} (subst hom-comp hom-≡ comp) compʹ

  ≡-id : ∀ {ℓ ℓʹ : Level} {C : Set ℓ} {hom homʹ : hom-set C ℓʹ} (hom-≡ : hom ≡ homʹ)
      → hom-comp-id hom → hom-comp-id homʹ → Set (ℓ ⊔ ℓʹ)
  ≡-id {_} {_} {_} {_} {homʹ} hom-≡ id idʹ = _≡_ {A = hom-comp-id homʹ} (subst hom-comp-id hom-≡ id) idʹ

  ≡-assoc : ∀ {ℓ ℓʹ : Level} {C : Set ℓ} {hom homʹ : hom-set C ℓʹ} (hom-≡ : hom ≡ homʹ)
              {comp : hom-comp hom} {compʹ : hom-comp homʹ} (comp-≡ : ≡-comp hom-≡ comp compʹ)
         → hom-comp-assoc hom comp → hom-comp-assoc homʹ compʹ → Set (ℓ ⊔ ℓʹ)
  ≡-assoc {_} {_} {_} {_} {homʹ} hom-≡ {_} {compʹ} comp-≡ assoc assocʹ =
    _≡_ {A = hom-comp-assoc homʹ compʹ} (subst-dep₂ hom-comp-assoc hom-≡ comp-≡ assoc) assocʹ
  
  ident-subst : ∀ {ℓ ℓʹ : Level} {C : Set ℓ} {hom homʹ : hom-set C ℓʹ}
                  {comp : hom-comp hom} {compʹ : hom-comp homʹ} {id : hom-comp-id hom} {idʹ : hom-comp-id homʹ}
             → (P : {C : Set ℓ} → (hom : hom-set C ℓʹ) → hom-comp hom → hom-comp-id hom → Set (ℓ ⊔ ℓʹ))
             → (hom-≡ : hom ≡ homʹ) → ≡-comp hom-≡ comp compʹ → ≡-id hom-≡ id idʹ
             → P hom comp id → P homʹ compʹ idʹ
  ident-subst _ refl refl refl x = x

  ≡-ident : ∀ {ℓ ℓʹ : Level} {C : Set ℓ} {hom homʹ : hom-set C ℓʹ} (hom-≡ : hom ≡ homʹ)
              {comp : hom-comp hom} {compʹ : hom-comp homʹ} (comp-≡ : ≡-comp hom-≡ comp compʹ)
              {id : hom-comp-id hom} {idʹ : hom-comp-id homʹ} (id-≡ : ≡-id hom-≡ id idʹ)
         → (P : {C : Set ℓ} → (hom : hom-set C ℓʹ) → hom-comp hom → hom-comp-id hom → Set (ℓ ⊔ ℓʹ))
         → P hom comp id → P homʹ compʹ idʹ → Set (ℓ ⊔ ℓʹ)
  ≡-ident {_} {_} {_} {_} {homʹ} hom-≡ {_} {compʹ} comp-≡ {_} {idʹ} id-≡ P ident identʹ =
    _≡_ {A = P homʹ compʹ idʹ} (ident-subst P hom-≡ comp-≡ id-≡ ident) identʹ

cat-cong : ∀ {ℓ ℓʹ : Level} {C : Set ℓ} {hom homʹ : hom-set C ℓʹ} (hom-≡ : hom ≡ homʹ)
             {comp : hom-comp hom} {compʹ : hom-comp homʹ} (comp-≡ : ≡-comp hom-≡ comp compʹ)
             {id : hom-comp-id hom} {idʹ : hom-comp-id homʹ} (id-≡ : ≡-id hom-≡ id idʹ)
             {assoc : hom-comp-assoc hom comp} {assocʹ : hom-comp-assoc homʹ compʹ}
             (assoc-≡ : ≡-assoc hom-≡ comp-≡ assoc assocʹ)
             {identˡ : hom-comp-identˡ hom comp id} {identˡʹ : hom-comp-identˡ homʹ compʹ idʹ}
             (identˡ-≡ : ≡-ident hom-≡ comp-≡ id-≡ hom-comp-identˡ identˡ identˡʹ)
             {identʳ : hom-comp-identʳ hom comp id} {identʳʹ : hom-comp-identʳ homʹ compʹ idʹ}
             (identʳ-≡ : ≡-ident hom-≡ comp-≡ id-≡ hom-comp-identʳ identʳ identʳʹ)
        → NewCat hom comp id assoc identˡ identʳ ≡ NewCat homʹ compʹ idʹ assocʹ identˡʹ identʳʹ
cat-cong refl refl refl refl refl refl = refl