open import Cat.Diagram.Limit.Finite
open import Cat.Diagram.Pullback
open import Cat.Diagram.Product
open import Cat.Prelude

import Cat.Diagram.Congruence
import Cat.Internal.Base
import Cat.Reasoning

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

open Cat.Diagram.Congruence fc
open Cat.Internal.Base C
open Cat.Reasoning C
private module fc = Finitely-complete fc
open Pullbacks C fc.pullbacks
open Binary-products C fc.products

open Internal-cat
open Internal-cat-on
open Internal-hom


# Internal categories from congruencesπ

Let $\mathcal{C}$ be a finitely complete category, and recall that a congruence in $\mathcal{C}$ 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 $x \to y$ if and only if $x$ and $y$ 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 $A$, and the object of morphisms is given by the subobject of $A \times A$ 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 _  β‘β¨ unpair-trans _ β©β‘
β¨ relβ β f .ihom , relβ β has-refl β y β© β‘β¨ apβ β¨_,_β© (f .has-src) (pulll refl-pβ β idl _) β©β‘
β¨ x , y β©                                β‘Λβ¨ β¨β©-unique _ (assoc _ _ _ β f .has-src) (assoc _ _ _ β f .has-tgt) β©β‘Λ
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 _  β‘β¨ unpair-trans _ β©β‘
β¨ relβ β has-refl β x , relβ β f .ihom β© β‘β¨ apβ β¨_,_β© (pulll refl-pβ β idl _) (f .has-tgt) β©β‘
β¨ x , y β©                                β‘Λβ¨ β¨β©-unique _ (assoc _ _ _ β f .has-src) (assoc _ _ _ β f .has-tgt) β©β‘Λ
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 _                 β‘β¨ unpair-trans _ β©β‘
β¨ relβ β has-trans β RΓR.universal _ , relβ β f .ihom β© β‘β¨ apβ β¨_,_β© (pulll trans-pβ β pullr RΓR.pββuniversal) refl β©β‘
β¨ relβ β h .ihom , relβ β f .ihom β©                     β‘Λβ¨ apβ β¨_,_β© refl (pulll trans-pβ β pullr RΓR.pββuniversal) β©β‘Λ
β¨ relβ β h .ihom , relβ β has-trans β RΓR.universal _ β© β‘Λβ¨ unpair-trans _ β©β‘Λ
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))