module Cat.Morphism.Factorisation where

Factorisations🔗

Let be two classes of morphisms of An factorisation of a morphism consists of an object and a pair of morphisms such that and

  record Factorisation {a b} (f : C.Hom a b) : Type (o    ℓl  ℓr) where
    field
      mid     : C.Ob
      left    : C.Hom a mid
      right   : C.Hom mid b
      left∈L  : left  L
      right∈R : right  R
      factors : f  right C.∘ left

Properties of factorisations🔗

If is monic and factors as then must also be monic.

  factor-monic→left-monic
    :  {x y} {f : C.Hom x y}
     (f-fac : Factorisation C L R f)
     C.is-monic f
     C.is-monic (f-fac .left)
  factor-monic→left-monic {f = f} f-fac f-monic = C.monic-cancell $
    C.subst-is-monic (f-fac .factors) f-monic

If is epic and factors as then must also be epic.

  factor-epic→right-epic
    :  {x y} {f : C.Hom x y}
     (f-fac : Factorisation C L R f)
     C.is-epic f
     C.is-epic (f-fac .right)
  factor-epic→right-epic {f = f} f-fac f-epic = C.epic-cancelr $
    C.subst-is-epic (f-fac .factors) f-epic