{-# OPTIONS --without-K --safe #-}
open import Categories.Category
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
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
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