module Cat.Internal.Instances.Congruence
{o β} {C : Precategory o β}
(fc : Finitely-complete C)
where

# Internal categories from congruencesπ

Let be a finitely complete category, and recall that a congruence in is an internalized notion of equivalence relation. Intuitively, we should be able to turn this into an internal category, where we have an internal morphism if and only if and are congruent.

EquivRel : β {A} β Congruence-on A β Internal-cat
EquivRel {A} cong = icat where
open Congruence-on cong
private module RΓR = Pullback (fc.pullbacks relβ relβ)

The object of objects of the internal category will simply be and the object of morphisms is given by the subobject of associated with the congruence. The source and target maps are given by projections from the aforementioned subobject.

icat : Internal-cat
icat .Cβ = A
icat .Cβ = domain
icat .src = relβ
icat .tgt = relβ

As aluded to earlier, the identity morphism is given by reflexivity, and composition by transitivity.

icat .has-internal-cat .idi x .ihom = has-refl β x
icat .has-internal-cat .idi x .has-src = cancell refl-pβ
icat .has-internal-cat .idi x .has-tgt = cancell refl-pβ
icat .has-internal-cat ._βi_ f g .ihom =
has-trans β pullback.universal _ _ (f .has-src β sym (g .has-tgt))
icat .has-internal-cat ._βi_ f g .has-src =
pulll trans-pβ
Β·Β· pullr RΓR.pββuniversal
Β·Β· g .has-src
icat .has-internal-cat ._βi_ f g .has-tgt =
pulll trans-pβ
Β·Β· pullr RΓR.pββuniversal
Β·Β· f .has-tgt
Proving the category equations is an exercise in shuffling around products and pullbacks.
icat .has-internal-cat .idli {x = x} {y = y} f =
Internal-hom-path $has-is-monic _ _$
inclusion β has-trans β RΓR.universal _  β‘
β¨ relβ β f .ihom , relβ β has-refl β y β©
β¨ x , y β©                                β‘Λ
inclusion β f .ihom                      β
icat .has-internal-cat .idri {x = x} {y = y} f =
Internal-hom-path $has-is-monic _ _$
inclusion β has-trans β RΓR.universal _  β‘
β¨ relβ β has-refl β x , relβ β f .ihom β©
β¨ x , y β©                                β‘Λ
inclusion β f .ihom β
icat .has-internal-cat .associ {w = w} {x = x} {y = y} {z = z} f g h =
Internal-hom-path $has-is-monic _ _$
inclusion β has-trans β RΓR.universal _                 β‘
β¨ relβ β has-trans β RΓR.universal _ , relβ β f .ihom β©
β¨ relβ β h .ihom , relβ β f .ihom β©
β¨ relβ β h .ihom , relβ β has-trans β RΓR.universal _ β© β‘Λ
inclusion β has-trans β RΓR.universal _ β
icat .has-internal-cat .idi-nat Ο =
Internal-hom-path (sym (assoc _ _ _))
icat .has-internal-cat .βi-nat f g Ο =
Internal-hom-path \$
sym (assoc _ _ _)
β ap (has-trans β_) (RΓR.unique (pulll RΓR.pββuniversal) (pulll RΓR.pββuniversal))