{-# OPTIONS --without-K --safe #-}
open import Categories.Category

-- Properties relating Initial and Terminal Objects,
-- Product / Coproduct, Zero objects, and Kernel / Cokernel via op
module Categories.Object.Duality {o ℓ e} (C : Category o ℓ e) where

open Category C

open import Level
open import Relation.Binary.PropositionalEquality as ≡ using (_≡_)

open import Categories.Morphism C
open import Categories.Object.Terminal op
open import Categories.Object.Initial C
open import Categories.Object.Product op
open import Categories.Object.Coproduct C

open import Categories.Object.Zero

import Categories.Object.Kernel as Kernels
import Categories.Object.Cokernel as Cokernels

private
  variable
    A B X Z : Obj
    f g k : A ⇒ B

IsInitial⇒coIsTerminal : IsInitial X → IsTerminal X
IsInitial⇒coIsTerminal is⊥ = record
  { !        = !
  ; !-unique = !-unique
  }
  where open IsInitial is⊥

⊥⇒op⊤ : Initial → Terminal
⊥⇒op⊤ i = record
  { ⊤             = ⊥
  ; ⊤-is-terminal = IsInitial⇒coIsTerminal ⊥-is-initial
  }
  where open Initial i

coIsTerminal⇒IsInitial : IsTerminal X → IsInitial X
coIsTerminal⇒IsInitial is⊤ = record
  { !        = !
  ; !-unique = !-unique
  }
  where open IsTerminal is⊤

op⊤⇒⊥ : Terminal → Initial
op⊤⇒⊥ t = record
  { ⊥            = ⊤
  ; ⊥-is-initial = coIsTerminal⇒IsInitial ⊤-is-terminal
  }
  where open Terminal t

Coproduct⇒coProduct : Coproduct A B → Product A B
Coproduct⇒coProduct A+B = record
  { A×B      = A+B.A+B
  ; π₁       = A+B.i₁
  ; π₂       = A+B.i₂
  ; ⟨_,_⟩    = A+B.[_,_]
  ; project₁ = A+B.inject₁
  ; project₂ = A+B.inject₂
  ; unique   = A+B.unique
  }
  where
  module A+B = Coproduct A+B

coProduct⇒Coproduct : ∀ {A B} → Product A B → Coproduct A B
coProduct⇒Coproduct A×B = record
  { A+B     = A×B.A×B
  ; i₁      = A×B.π₁
  ; i₂      = A×B.π₂
  ; [_,_]   = A×B.⟨_,_⟩
  ; inject₁ = A×B.project₁
  ; inject₂ = A×B.project₂
  ; unique  = A×B.unique
  }
  where
  module A×B = Product A×B

-- Zero objects are autodual
IsZero⇒coIsZero : IsZero C Z → IsZero op Z
IsZero⇒coIsZero is-zero = record
  { isInitial = record { ! = ! ; !-unique = !-unique }
  ; isTerminal = record { ! = ¡ ; !-unique = ¡-unique }
  }
  where
    open IsZero is-zero

coIsZero⇒IsZero : IsZero op Z → IsZero C Z
coIsZero⇒IsZero co-is-zero = record
  { isInitial = record { ! = ! ; !-unique = !-unique }
  ; isTerminal = record { ! = ¡ ; !-unique = ¡-unique }
  }
  where
    open IsZero co-is-zero

coZero⇒Zero : Zero op → Zero C
coZero⇒Zero zero = record
  { 𝟘 = 𝟘
  ; isZero = coIsZero⇒IsZero isZero
  }
  where
    open Zero zero

Zero⇒coZero : Zero C → Zero op
Zero⇒coZero zero = record
  { 𝟘 = 𝟘
  ; isZero = IsZero⇒coIsZero isZero
  }
  where
    open Zero zero

-- Tests to ensure that dualities are involutive up to definitional equality.
private
  coIsTerminal⟺IsInitial : (⊥ : IsInitial X) → coIsTerminal⇒IsInitial (IsInitial⇒coIsTerminal ⊥) ≡ ⊥
  coIsTerminal⟺IsInitial _ = ≡.refl

  IsInitial⟺coIsTerminal : (⊤ : IsTerminal X) → IsInitial⇒coIsTerminal (coIsTerminal⇒IsInitial ⊤) ≡ ⊤
  IsInitial⟺coIsTerminal _ = ≡.refl

  ⊥⟺op⊤ : (⊤ : Terminal) → ⊥⇒op⊤ (op⊤⇒⊥ ⊤) ≡ ⊤
  ⊥⟺op⊤ _ = ≡.refl

  op⊤⟺⊥ : (⊥ : Initial) → op⊤⇒⊥ (⊥⇒op⊤ ⊥) ≡ ⊥
  op⊤⟺⊥ _ = ≡.refl

  Coproduct⟺coProduct : (p : Product A B) → Coproduct⇒coProduct (coProduct⇒Coproduct p) ≡ p
  Coproduct⟺coProduct _ = ≡.refl

  coProduct⟺Coproduct : (p : Coproduct A B) → coProduct⇒Coproduct (Coproduct⇒coProduct p) ≡ p
  coProduct⟺Coproduct _ = ≡.refl

  coIsZero⟺IsZero : {zero : IsZero op Z} → IsZero⇒coIsZero (coIsZero⇒IsZero zero) ≡ zero
  coIsZero⟺IsZero = ≡.refl

  IsZero⟺coIsZero : ∀ {Z} {zero : IsZero C Z} → coIsZero⇒IsZero (IsZero⇒coIsZero zero) ≡ zero
  IsZero⟺coIsZero = ≡.refl

  coZero⟺Zero : ∀ {zero : Zero op} → Zero⇒coZero (coZero⇒Zero zero) ≡ zero
  coZero⟺Zero = ≡.refl

  Zero⟺coZero : ∀ {zero : Zero C} → coZero⇒Zero (Zero⇒coZero zero) ≡ zero
  Zero⟺coZero = ≡.refl

module _ (𝟎 : Zero C) where
  open Kernels (Zero⇒coZero 𝟎)
  open Cokernels 𝟎

  coIsKernel⇒IsCokernel : IsKernel k f → IsCokernel f k
  coIsKernel⇒IsCokernel isKernel = record
    { commute = commute
    ; universal = universal
    ; factors = factors
    ; unique = unique
    }
    where
      open IsKernel isKernel

  IsCokernel⇒coIsKernel : IsCokernel f k → IsKernel k f
  IsCokernel⇒coIsKernel isCokernel = record
    { commute = commute
    ; universal = universal
    ; factors = factors
    ; unique = unique
    }
    where
      open IsCokernel isCokernel

  coKernel⇒Cokernel : Kernel f → Cokernel f
  coKernel⇒Cokernel k = record
    { cokernel⇒ = kernel⇒
    ; isCokernel = coIsKernel⇒IsCokernel isKernel
    }
    where
      open Kernel k

  Cokernel⇒coKernel : Cokernel f → Kernel f
  Cokernel⇒coKernel k = record
    { kernel⇒ = cokernel⇒
    ; isKernel = IsCokernel⇒coIsKernel isCokernel
    }
    where
      open Cokernel k

  private
    coIsKernel⟺IsCokernel : ∀ {isKernel : IsKernel k f} → IsCokernel⇒coIsKernel (coIsKernel⇒IsCokernel isKernel) ≡ isKernel
    coIsKernel⟺IsCokernel = ≡.refl

    IsCokernel⟺coIsKernel : ∀ {isCokernel : IsCokernel f k} → coIsKernel⇒IsCokernel (IsCokernel⇒coIsKernel isCokernel) ≡ isCokernel
    IsCokernel⟺coIsKernel = ≡.refl

    coKernel⟺Cokernel : ∀ {kernel : Kernel f} → Cokernel⇒coKernel (coKernel⇒Cokernel kernel) ≡ kernel
    coKernel⟺Cokernel = ≡.refl

    Cokernel⟺coKernel : ∀ {cokernel : Cokernel f} → coKernel⇒Cokernel (Cokernel⇒coKernel cokernel) ≡ cokernel
    Cokernel⟺coKernel = ≡.refl