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 _  β‰‘βŸ¨ 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))