-- {-# OPTIONS --lossy-unification #-}
open import Cat.Functor.FullSubcategory
open import Cat.Morphism.Factorisation
open import Cat.Morphism.StrongEpi
open import Cat.Diagram.Pullback
open import Cat.Diagram.Product
open import Cat.Instances.Slice
open import Cat.Prelude
open import Cat.Regular

import Cat.Displayed.Instances.Subobjects
import Cat.Reasoning as Cr

module Cat.Regular.Image
{o β} {C : Precategory o β}
(reg : is-regular C)
where

open Binary-products C (reg .is-regular.lex.products)
open Cat.Displayed.Instances.Subobjects C
open is-regular reg
open Factorisation
open Pullback
open /-Hom
open /-Obj
open Cr C


# Images in regular categoriesπ

This module provides tools for working with the image factorisation of morphisms in regular categories, regarded as subobjects of the mapβs codomain. We start by defining a Subobject of standing for whenever

Im : β {x y} (f : Hom x y) β Subobject y
Im f .domain = _
Im f .map    = factor f .forget
Im f .monic  = out! (factor f .forgetβM)


We may then use this to rephrase the universal property of as the initial subobject through which factors.

Im-universal
: β {x y} (f : Hom x y)
β (m : Subobject y) {e : Hom x (m .domain)}
β f β‘ m .map β e
β Im f β€β m
Im-universal f m {e = e} p = r where
the-lift = out! {pa = is-strong-epi-is-prop C _} (factor f .mediateβE) .snd
record { Subobject m } (sym (factor f .factors) β p)

r : _ β€β _
r .map = the-lift .centre .fst
r .sq  = idl _ β sym (the-lift .centre .snd .snd)


An important fact that will be used in calculating associativity for relations in regular categories is that precomposing with a strong epimorphism preserves images. Intuitively, this is because a strong epimorphism expresses as a quotient, but this decomposition does not alter the image of a map

image-pre-cover
: β {a b c}
β (f : Hom b c)
β (g : Hom a b)
β is-strong-epi C g
β (Im f) Sub.β (Im (f β g))
image-pre-cover {a = a} {b} {c} f g g-covers = Sub-antisym imfβ€imfg imfgβ€imf where
imfgβ€imf : Im (f β g) β€β Im f
imfgβ€imf = Im-universal _ _ (pushl (factor f .factors))

the-lift : Ξ£ (Hom b im[ f β g ]) _
the-lift = g-covers .snd
(β€ββmono imfgβ€imf)
{factor (f β g) .mediate}
{factor f .mediate}
(out! (factor f .forgetβM) _ _ (sym (pulll (sym (imfgβ€imf .sq) β idl _) β sym (factor (f β g) .factors) β pushl (factor f .factors)))) .centre

inverse : is-invertible (imfgβ€imf .map)
inverse = is-strong-epiβis-extremal-epi C (out! {pa = is-strong-epi-is-prop C _} (factor f .mediateβE))
(β€ββmono imfgβ€imf) (the-lift .fst) (sym (the-lift .snd .snd))

imfβ€imfg : Im f β€β Im (f β g)
imfβ€imfg .map = inverse .is-invertible.inv
imfβ€imfg .sq = invertibleβepic inverse _ _ \$
pullr (sym (imfgβ€imf .sq) β idl _)
β sym (cancelr (inverse .is-invertible.invr) β introl refl)