open import Cat.Base

import Cat.Morphism

module Cat.Morphism.Duality {o β„“} (π’ž : Precategory o β„“) where

private
  module π’ž = Cat.Morphism π’ž
  module π’ž^op = Cat.Morphism (π’ž ^op)

private variable
  a b c d : π’ž.Ob
  f g : π’ž.Hom a b

Duality of morphism classesπŸ”—

In this file we prove that morphisms classes in a category correspond to their duals in the opposite category. There is very little interesting mathematical content in this file; it is pure boilerplate.

We start by showing that monos and epis are dual.

co-monoβ†’epi : a π’ž^op.β†ͺ b β†’ b π’ž.β†  a
co-monoβ†’epi f .Cat.Morphism.mor = π’ž^op.mor f
co-monoβ†’epi f .Cat.Morphism.epic = π’ž^op.monic f

epiβ†’co-mono : b π’ž.β†  a β†’ a π’ž^op.β†ͺ b
epiβ†’co-mono f .Cat.Morphism.mor = π’ž.mor f
epiβ†’co-mono f .Cat.Morphism.monic = π’ž.epic f

co-epiβ†’mono : a π’ž^op.β†  b β†’ b π’ž.β†ͺ a
co-epiβ†’mono f .Cat.Morphism.mor = π’ž^op.mor f
co-epiβ†’mono f .Cat.Morphism.monic = π’ž^op.epic f

monoβ†’co-epi : b π’ž.β†ͺ a β†’ a π’ž^op.β†  b
monoβ†’co-epi f .Cat.Morphism.mor = π’ž.mor f
monoβ†’co-epi f .Cat.Morphism.epic = π’ž.monic f

Next, sections and retractions.

co-sectionβ†’retract : π’ž^op.has-section f β†’ π’ž.has-retract f
co-sectionβ†’retract f .Cat.Morphism.retract = π’ž^op.section f
co-sectionβ†’retract f .Cat.Morphism.is-retract = π’ž^op.is-section f

retractβ†’co-section : π’ž.has-retract f β†’ π’ž^op.has-section f
retractβ†’co-section f .Cat.Morphism.section = π’ž.retract f
retractβ†’co-section f .Cat.Morphism.is-section = π’ž.is-retract f

co-retractβ†’section : π’ž^op.has-retract f β†’ π’ž.has-section f
co-retractβ†’section f .Cat.Morphism.section = π’ž^op.retract f
co-retractβ†’section f .Cat.Morphism.is-section = π’ž^op.is-retract f

sectionβ†’co-retract : π’ž.has-section f β†’ π’ž^op.has-retract f
sectionβ†’co-retract f .Cat.Morphism.retract = π’ž.section f
sectionβ†’co-retract f .Cat.Morphism.is-retract = π’ž.is-section f

Next, we show that invertible morphisms are self-dual.

co-inversesβ†’inverses : π’ž^op.Inverses f g β†’ π’ž.Inverses f g
co-inverses→inverses i .Cat.Morphism.Inverses.invl =
  π’ž^op.Inverses.invr i
co-inverses→inverses i .Cat.Morphism.Inverses.invr =
  π’ž^op.Inverses.invl i

inversesβ†’co-inverses : π’ž.Inverses f g β†’ π’ž^op.Inverses f g
inverses→co-inverses i .Cat.Morphism.Inverses.invl =
  π’ž.Inverses.invr i
inverses→co-inverses i .Cat.Morphism.Inverses.invr =
  π’ž.Inverses.invl i

co-invertibleβ†’invertible : π’ž^op.is-invertible f β†’ π’ž.is-invertible f
co-invertible→invertible i .Cat.Morphism.is-invertible.inv =
  π’ž^op.is-invertible.inv i
co-invertible→invertible i .Cat.Morphism.is-invertible.inverses =
  co-inversesβ†’inverses (π’ž^op.is-invertible.inverses i)

invertibleβ†’co-invertible : π’ž.is-invertible f β†’ π’ž^op.is-invertible f
invertible→co-invertible i .Cat.Morphism.is-invertible.inv =
  π’ž.is-invertible.inv i
invertible→co-invertible i .Cat.Morphism.is-invertible.inverses =
  inversesβ†’co-inverses (π’ž.is-invertible.inverses i)

co-isoβ†’iso : a π’ž^op.β‰… b β†’ b π’ž.β‰… a
co-isoβ†’iso f .Cat.Morphism.to = π’ž^op.to f
co-isoβ†’iso f .Cat.Morphism.from = π’ž^op.from f
co-isoβ†’iso f .Cat.Morphism.inverses = co-inversesβ†’inverses (π’ž^op.inverses f)

isoβ†’co-iso : b π’ž.β‰… a β†’ a π’ž^op.β‰… b
isoβ†’co-iso f .Cat.Morphism.to = π’ž.to f
isoβ†’co-iso f .Cat.Morphism.from = π’ž.from f
isoβ†’co-iso f .Cat.Morphism.inverses = inversesβ†’co-inverses (π’ž.inverses f)