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

Internal categories from congruencesπŸ”—

Let C\mathcal{C} be a finitely complete category, and recall that a congruence in C\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→yx \to y if and only if xx and yy 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 AA, and the object of morphisms is given by the subobject of AΓ—AA \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))