{-# OPTIONS --without-K --safe #-}

open import Categories.Category

module Categories.Morphism.Duality {o ℓ e} (C : Category o ℓ e) where

open import Relation.Binary.PropositionalEquality using (_≡_; refl)

open Category C

import Categories.Morphism as M
private
  module Op = M op
open M C

open import Categories.Morphism.Properties C

private
  variable
    A B X Y : Obj
    f g h : A ⇒ B

Mono⇒op-Epi : Mono f → Op.Epi f
Mono⇒op-Epi mono = mono

Epi⇒op-Mono : Epi f → Op.Mono f
Epi⇒op-Mono epi = epi

Iso⇒op-Iso : Iso f g → Op.Iso g f
Iso⇒op-Iso iso = record
  { isoˡ = isoˡ
  ; isoʳ = isoʳ
  }
  where open Iso iso

op-Iso⇒Iso : Op.Iso g f → Iso f g
op-Iso⇒Iso iso = record
  { isoˡ = isoˡ
  ; isoʳ = isoʳ
  }
  where open Op.Iso iso

≅⇒op-≅ : A ≅ B → A Op.≅ B
≅⇒op-≅ A≅B = record
  { from = to
  ; to   = from
  ; iso  = Iso⇒op-Iso iso
  }
  where open _≅_ A≅B

op-≅⇒≅ : A Op.≅ B → A ≅ B
op-≅⇒≅ A≅B = record
  { from = to
  ; to   = from
  ; iso  = op-Iso⇒Iso iso
  }
  where open Op._≅_ A≅B


module MorphismDualityConversionProperties where
  private
    op-Iso-involutive : ∀(iso : Iso f g) → op-Iso⇒Iso (Iso⇒op-Iso iso) ≡ iso
    op-Iso-involutive _ = refl

    op-≅-involutive : ∀(A′ B′ : Obj) → (A′≅B′ : A′ ≅ B′)
                       → op-≅⇒≅ (≅⇒op-≅ A′≅B′) ≡ A′≅B′
    op-≅-involutive _ _ _ = refl