open import Cat.Displayed.Base
open import Cat.Prelude

import Cat.Displayed.Reasoning
import Cat.Reasoning

module Cat.Displayed.Morphism
  {o ℓ o′ ℓ′}
  {ℬ : Precategory o ℓ}
  (ℰ : Displayed ℬ o′ ℓ′)
  where

Displayed Morphisms🔗

This module defines the displayed analogs of monomorphisms, epimorphisms, and isomorphisms.

Monos🔗

Displayed monomorphisms have the the same left-cancellation properties as their non-displayed counterparts. However, they must be displayed over a monomorphism in the base.

is-monic[_]
  : ∀ {a′ : Ob[ a ]} {b′ : Ob[ b ]} {f : Hom a b}
  → is-monic f → Hom[ f ] a′ b′
  → Type _
is-monic[_] {a = a} {a′ = a′} {f = f} mono f′ =
  ∀ {c c′} {g h : Hom c a}
  → (g′ : Hom[ g ] c′ a′) (h′ : Hom[ h ] c′ a′)
  → (p : f ∘ g ≡ f ∘ h)
  → f′ ∘′ g′ ≡[ p ] f′ ∘′ h′
  → g′ ≡[ mono g h p ] h′

is-monic[]-is-prop
  : ∀ {a′ : Ob[ a ]} {b′ : Ob[ b ]} {f : Hom a b}
  → (mono : is-monic f) → (f′ : Hom[ f ] a′ b′)
  → is-prop (is-monic[ mono ] f′)
is-monic[]-is-prop {a′ = a′} mono f′ mono[] mono[]′ i {c′ = c′} g′ h′ p p′ =
  is-set→squarep (λ i j → Hom[ mono _ _ p j ]-set c′ a′)
    refl (mono[] g′ h′ p p′) (mono[]′ g′ h′ p p′) refl i

record _↪[_]_
  {a b} (a′ : Ob[ a ]) (f : a ↪ b) (b′ : Ob[ b ])
  : Type (o ⊔ ℓ ⊔ o′ ⊔ ℓ′)
  where
  no-eta-equality
  field
    mor′ : Hom[ f .mor ] a′ b′
    monic′ : is-monic[ f .monic ] mor′

open _↪[_]_ public

Weak Monos🔗

When working in a displayed setting, we also have weaker versions of the morphism classes we are familiar with, wherein we can only left/right cancel morphisms that are displayed over the same morphism in the base. We denote these morphisms classes as “weak”.

is-weak-monic
  : ∀ {a′ : Ob[ a ]} {b′ : Ob[ b ]} {f : Hom a b}
  → Hom[ f ] a′ b′
  → Type _
is-weak-monic {a = a} {a′ = a′} {f = f} f′ =
  ∀ {c c′} {g : Hom c a}
  → (g′ g″ : Hom[ g ] c′ a′)
  → f′ ∘′ g′ ≡ f′ ∘′ g″
  → g′ ≡ g″

is-weak-monic-is-prop
  : ∀ {a′ : Ob[ a ]} {b′ : Ob[ b ]} {f : Hom a b}
  → (f′ : Hom[ f ] a′ b′)
  → is-prop (is-weak-monic f′)
is-weak-monic-is-prop f′ mono mono′ i g′ g″ p =
  is-prop→pathp (λ i → Hom[ _ ]-set _ _ g′ g″)
    (mono g′ g″ p) (mono′ g′ g″ p) i

record weak-mono-over
  {a b} (f : Hom a b) (a′ : Ob[ a ]) (b′ : Ob[ b ])
  : Type (o ⊔ ℓ ⊔ o′ ⊔ ℓ′)
  where
  no-eta-equality
  field
    mor′ : Hom[ f ] a′ b′
    weak-monic : is-weak-monic mor′

open weak-mono-over public

Epis🔗

Displayed epimorphisms are defined in a similar fashion.

is-epic[_]
  : ∀ {a′ : Ob[ a ]} {b′ : Ob[ b ]} {f : Hom a b}
  → is-epic f → Hom[ f ] a′ b′
  → Type _
is-epic[_] {b = b} {b′ = b′} {f = f} epi f′ =
  ∀ {c} {c′} {g h : Hom b c}
  → (g′ : Hom[ g ] b′ c′) (h′ : Hom[ h ] b′ c′)
  → (p : g ∘ f ≡ h ∘ f)
  → g′ ∘′ f′ ≡[ p ] h′ ∘′ f′
  → g′ ≡[ epi g h p ] h′

is-epic[]-is-prop
  : ∀ {a′ : Ob[ a ]} {b′ : Ob[ b ]} {f : Hom a b}
  → (epi : is-epic f) → (f′ : Hom[ f ] a′ b′)
  → is-prop (is-epic[ epi ] f′)
is-epic[]-is-prop {b′ = b′} epi f′ epi[] epi[]′ i {c′ = c′} g′ h′ p p′ =
  is-set→squarep (λ i j → Hom[ epi _ _ p j ]-set b′ c′)
    refl (epi[] g′ h′ p p′) (epi[]′ g′ h′ p p′) refl i

record _↠[_]_
  {a b} (a′ : Ob[ a ]) (f : a ↠ b) (b′ : Ob[ b ])
  : Type (o ⊔ ℓ ⊔ o′ ⊔ ℓ′)
  where
  no-eta-equality
  field
    mor′ : Hom[ f .mor ] a′ b′
    epic′ : is-epic[ f .epic ] mor′

open _↠[_]_ public

Weak Epis🔗

We can define a weaker notion of epis that is dual to the definition of a weak mono.

is-weak-epic
  : ∀ {a′ : Ob[ a ]} {b′ : Ob[ b ]} {f : Hom a b}
  → Hom[ f ] a′ b′
  → Type _
is-weak-epic {b = b} {b′ = b′} {f = f} f′ =
  ∀ {c c′} {g : Hom b c}
  → (g′ g″ : Hom[ g ] b′ c′)
  → g′ ∘′ f′ ≡ g″ ∘′ f′
  → g′ ≡ g″

is-weak-epic-is-prop
  : ∀ {a′ : Ob[ a ]} {b′ : Ob[ b ]} {f : Hom a b}
  → (f′ : Hom[ f ] a′ b′)
  → is-prop (is-weak-monic f′)
is-weak-epic-is-prop f′ epi epi′ i g′ g″ p =
  is-prop→pathp (λ i → Hom[ _ ]-set _ _ g′ g″)
    (epi g′ g″ p) (epi′ g′ g″ p) i

record weak-epi-over
  {a b} (f : Hom a b) (a′ : Ob[ a ]) (b′ : Ob[ b ])
  : Type (o ⊔ ℓ ⊔ o′ ⊔ ℓ′)
  where
  no-eta-equality
  field
    mor′ : Hom[ f ] a′ b′
    weak-epic : is-weak-epic mor′

open weak-epi-over public

Sections🔗

Following the same pattern as before, we define a notion of displayed sections.

_section-of[_]_
  : ∀ {x y} {s : Hom y x} {r : Hom x y}
  → ∀ {x′ y′} (s′ : Hom[ s ] y′ x′) → s section-of r → (r′ : Hom[ r ] x′ y′)
  → Type _
s′ section-of[ p ] r′ = r′ ∘′ s′ ≡[ p ] id′

record has-section[_]
  {x y x′ y′} {r : Hom x y} (sect : has-section r) (r′ : Hom[ r ] x′ y′)
  : Type ℓ′
  where
  no-eta-equality
  field
    section′ : Hom[ sect .section ] y′ x′
    is-section′ : section′ section-of[ sect .is-section ] r′

open has-section[_] public

We also distinguish the sections that are displayed over the identity morphism; these are known as “vertical sections”.

_section-of↓_
  : ∀ {x} {x′ x″ : Ob[ x ]} (s′ : Hom[ id ] x″ x′) → (r : Hom[ id ] x′ x″)
  → Type _
s′ section-of↓ r′ = s′ section-of[ idl id ] r′

has-section↓ : ∀ {x} {x′ x″ : Ob[ x ]} (r′ : Hom[ id ] x′ x″) → Type _
has-section↓ r′ = has-section[ id-has-section ] r′

Retracts🔗

We can do something similar for retracts.

_retract-of[_]_
  : ∀ {x y} {s : Hom y x} {r : Hom x y}
  → ∀ {x′ y′} (r′ : Hom[ r ] x′ y′) → r retract-of s → (s′ : Hom[ s ] y′ x′)
  → Type _
r′ retract-of[ p ] s′ = r′ ∘′ s′ ≡[ p ] id′


record has-retract[_]
  {x y x′ y′} {s : Hom x y} (ret : has-retract s) (s′ : Hom[ s ] x′ y′)
  : Type ℓ′
  where
  no-eta-equality
  field
    retract′ : Hom[ ret .retract ] y′ x′
    is-retract′ : retract′ retract-of[ ret .is-retract ] s′

open has-retract[_] public

We also define vertical retracts in a similar manner as before.

_retract-of↓_
  : ∀ {x} {x′ x″ : Ob[ x ]} (r′ : Hom[ id ] x′ x″) → (s : Hom[ id ] x″ x′)
  → Type _
r′ retract-of↓ s′ = r′ retract-of[ idl id ] s′

has-retract↓ : ∀ {x} {x′ x″ : Ob[ x ]} (s′ : Hom[ id ] x″ x′) → Type _
has-retract↓ s′ = has-retract[ id-has-retract ] s′

Isos🔗

Displayed isomorphisms must also be defined over isomorphisms in the base.

record Inverses[_]
  {a b a′ b′} {f : Hom a b} {g : Hom b a}
  (inv : Inverses f g)
  (f′ : Hom[ f ] a′ b′) (g′ : Hom[ g ] b′ a′)
  : Type ℓ′
  where
  no-eta-equality
  field
    invl′ : f′ ∘′ g′ ≡[ Inverses.invl inv ] id′
    invr′ : g′ ∘′ f′ ≡[ Inverses.invr inv ] id′

record is-invertible[_]
  {a b a′ b′} {f : Hom a b}
  (f-inv : is-invertible f)
  (f′ : Hom[ f ] a′ b′)
  : Type ℓ′
  where
  no-eta-equality
  field
    inv′ : Hom[ is-invertible.inv f-inv ] b′ a′
    inverses′ : Inverses[ is-invertible.inverses f-inv ] f′ inv′

  open Inverses[_] inverses′ public

record _≅[_]_
  {a b} (a′ : Ob[ a ]) (i : a ≅ b) (b′ : Ob[ b ])
  : Type ℓ′
  where
  no-eta-equality
  field
    to′ : Hom[ i .to ] a′ b′
    from′ : Hom[ i .from ] b′ a′
    inverses′ : Inverses[ i .inverses ] to′ from′

  open Inverses[_] inverses′ public

open _≅[_]_ public

Since isomorphisms over the identity map will be of particular importance, we also define their own type: they are the vertical isomorphisms.

_≅↓_ : {x : Ob} (A B : Ob[ x ]) → Type ℓ′
_≅↓_ = _≅[ id-iso ]_

is-invertible↓ : {x : Ob} {x′ x″ : Ob[ x ]} → Hom[ id ] x′ x″ → Type _
is-invertible↓ = is-invertible[ id-invertible ]

make-invertible↓
  : ∀ {x} {x′ x″ : Ob[ x ]} {f′ : Hom[ id ] x′ x″}
  → (g′ : Hom[ id ] x″ x′)
  → f′ ∘′ g′ ≡[ idl _ ] id′
  → g′ ∘′ f′ ≡[ idl _ ] id′
  → is-invertible↓ f′
make-invertible↓ g′ p q .is-invertible[_].inv′ = g′
make-invertible↓ g′ p q .is-invertible[_].inverses′ .Inverses[_].invl′ = p
make-invertible↓ g′ p q .is-invertible[_].inverses′ .Inverses[_].invr′ = q

Like their non-displayed counterparts, existence of displayed inverses is a proposition.

Inverses[]-are-prop
  : ∀ {a b a′ b′} {f : Hom a b} {g : Hom b a}
  → (inv : Inverses f g)
  → (f′ : Hom[ f ] a′ b′) (g′ : Hom[ g ] b′ a′)
  → is-prop (Inverses[ inv ] f′ g′)
Inverses[]-are-prop inv f′ g′ inv[] inv[]′ i .Inverses[_].invl′ =
  is-set→squarep (λ i j → Hom[ Inverses.invl inv j ]-set _ _)
    refl (Inverses[_].invl′ inv[]) (Inverses[_].invl′ inv[]′) refl i
Inverses[]-are-prop inv f′ g′ inv[] inv[]′ i .Inverses[_].invr′ =
  is-set→squarep (λ i j → Hom[ Inverses.invr inv j ]-set _ _)
    refl (Inverses[_].invr′ inv[]) (Inverses[_].invr′ inv[]′) refl i

is-invertible[]-is-prop
  : ∀ {a b a′ b′} {f : Hom a b}
  → (f-inv : is-invertible f)
  → (f′ : Hom[ f ] a′ b′)
  → is-prop (is-invertible[ f-inv ] f′)
is-invertible[]-is-prop inv f′ p q = path where
  module inv = is-invertible inv
  module p = is-invertible[_] p
  module q = is-invertible[_] q

  inv≡inv′ : p.inv′ ≡ q.inv′
  inv≡inv′ =
    p.inv′                           ≡⟨ shiftr (insertr inv.invl) (insertr′ _ q.invl′) ⟩≡
    hom[] ((p.inv′ ∘′ f′) ∘′ q.inv′) ≡⟨ weave _ (eliml inv.invr) refl (eliml′ _ p.invr′) ⟩≡
    hom[] q.inv′                     ≡⟨ liberate _ ⟩≡
    q.inv′ ∎

  path : p ≡ q
  path i .is-invertible[_].inv′ = inv≡inv′ i
  path i .is-invertible[_].inverses′ =
    is-prop→pathp (λ i → Inverses[]-are-prop inv.inverses f′ (inv≡inv′ i))
      p.inverses′ q.inverses′ i

As in the non-displayed case, the identity isomorphism is always an iso. In fact, it is a vertical iso!

id-iso↓ : ∀ {x} {x′ : Ob[ x ]} → x′ ≅↓ x′
id-iso↓ = make-iso[ id-iso ] id′ id′ (idl′ id′) (idl′ id′)

Isomorphisms are also instances of sections and retracts.

inverses[]→to-has-section[]
  : ∀ {f : Hom a b} {g : Hom b a}
  → ∀ {a′ b′} {f′ : Hom[ f ] a′ b′} {g′ : Hom[ g ] b′ a′}
  → {inv : Inverses f g} → Inverses[ inv ] f′ g′
  → has-section[ inverses→to-has-section inv ] f′
inverses[]→to-has-section[] {g′ = g′} inv′ .section′ = g′
inverses[]→to-has-section[] inv′ .is-section′ = Inverses[_].invl′ inv′

inverses[]→from-has-section[]
  : ∀ {f : Hom a b} {g : Hom b a}
  → ∀ {a′ b′} {f′ : Hom[ f ] a′ b′} {g′ : Hom[ g ] b′ a′}
  → {inv : Inverses f g} → Inverses[ inv ] f′ g′
  → has-section[ inverses→from-has-section inv ] g′
inverses[]→from-has-section[] {f′ = f′} inv′ .section′ = f′
inverses[]→from-has-section[] inv′ .is-section′ = Inverses[_].invr′ inv′

inverses[]→to-has-retract[]
  : ∀ {f : Hom a b} {g : Hom b a}
  → ∀ {a′ b′} {f′ : Hom[ f ] a′ b′} {g′ : Hom[ g ] b′ a′}
  → {inv : Inverses f g} → Inverses[ inv ] f′ g′
  → has-retract[ inverses→to-has-retract inv ] f′
inverses[]→to-has-retract[] {g′ = g′} inv′ .retract′ = g′
inverses[]→to-has-retract[] inv′ .is-retract′ = Inverses[_].invr′ inv′

inverses[]→from-has-retract[]
  : ∀ {f : Hom a b} {g : Hom b a}
  → ∀ {a′ b′} {f′ : Hom[ f ] a′ b′} {g′ : Hom[ g ] b′ a′}
  → {inv : Inverses f g} → Inverses[ inv ] f′ g′
  → has-retract[ inverses→from-has-retract inv ] g′
inverses[]→from-has-retract[] {f′ = f′} inv′ .retract′ = f′
inverses[]→from-has-retract[] inv′ .is-retract′ = Inverses[_].invl′ inv′

iso[]→to-has-section[]
  : {f : a ≅ b} → (f′ : a′ ≅[ f ] b′)
  → has-section[ iso→to-has-section f ] (f′ .to′)
iso[]→to-has-section[] f′ .section′ = f′ .from′
iso[]→to-has-section[] f′ .is-section′ = f′ .invl′

iso[]→from-has-section[]
  : {f : a ≅ b} → (f′ : a′ ≅[ f ] b′)
  → has-section[ iso→from-has-section f ] (f′ .from′)
iso[]→from-has-section[] f′ .section′ = f′ .to′
iso[]→from-has-section[] f′ .is-section′ = f′ .invr′

iso[]→to-has-retract[]
  : {f : a ≅ b} → (f′ : a′ ≅[ f ] b′)
  → has-retract[ iso→to-has-retract f ] (f′ .to′)
iso[]→to-has-retract[] f′ .retract′ = f′ .from′
iso[]→to-has-retract[] f′ .is-retract′ = f′ .invr′

iso[]→from-has-retract[]
  : {f : a ≅ b} → (f′ : a′ ≅[ f ] b′)
  → has-retract[ iso→from-has-retract f ] (f′ .from′)
iso[]→from-has-retract[] f′ .retract′ = f′ .to′
iso[]→from-has-retract[] f′ .is-retract′ = f′ .invl′