{-# 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