module Cat.Functor.Hom.Properties where

Properties of hom functorsπŸ”—

This module contains a collection of useful facts about Hom functors, and the Yoneda embedding.

Monos and episπŸ”—

The Yoneda embedding preserves monomorphisms. Let be a mono, and let be a pair of natural transformations such that Equality of natural transformations is defined componentwise, so for every and we have Since is a mono, we can immediately deduce that

  γ‚ˆ-preserves-mono : is-monic f β†’ PSh[C].is-monic (γ‚ˆβ‚ C f)
  γ‚ˆ-preserves-mono f-mono Ξ± Ξ² p = ext Ξ» x px β†’
    f-mono (Ξ± .Ξ· x px) (Ξ² .Ξ· x px) (unext p x px)

Furthermore, the Yoneda embedding is fully faithful, so it reflects both monos and epis.

  γ‚ˆ-reflects-mono : PSh[C].is-monic (γ‚ˆβ‚ C f) β†’ is-monic f
  γ‚ˆ-reflects-mono = γ‚ˆ.faithfulβ†’reflects-mono (γ‚ˆ-is-faithful C)

  γ‚ˆ-reflects-epi : PSh[C].is-epic (γ‚ˆβ‚ C f) β†’ is-epic f
  γ‚ˆ-reflects-epi = γ‚ˆ.faithfulβ†’reflects-epi (γ‚ˆ-is-faithful C)

Likewise, the covariant Yoneda embedding takes epis to monos, reflects monos to epis, and vice versa.

  γ‚ˆcov-reverses-epi : is-epic f β†’ CoPSh[C].is-monic (γ‚ˆcov₁ C f)
  γ‚ˆcov-reverses-epi {f = f} f-epic Ξ± Ξ² p = ext Ξ» x px β†’
    f-epic (Ξ± .Ξ· x px) (Ξ² .Ξ· x px) (unext p x px)

  γ‚ˆcov-reflects-mono-to-epi : CoPSh[C].is-monic (γ‚ˆcov₁ C f) β†’ is-epic f
  γ‚ˆcov-reflects-mono-to-epi = γ‚ˆcov.faithfulβ†’reflects-mono (γ‚ˆcov-is-faithful C)

  γ‚ˆcov-reflects-epi-to-mono : CoPSh[C].is-epic (γ‚ˆcov₁ C f) β†’ is-monic f
  γ‚ˆcov-reflects-epi-to-mono = γ‚ˆcov.faithfulβ†’reflects-epi (γ‚ˆcov-is-faithful C)