open import 1Lab.Prelude

open import Data.Dec

module Data.Set.Coequaliser where

private variable
  β„“ β„“' : Level
  A B A' B' A'' B'' : Type β„“

Set coequalisersπŸ”—

In their most general form, colimits can be pictured as taking disjoint unions and then β€œgluing together” some parts. The β€œgluing together” part of that definition is where coequalisers come in: If you have parallel maps f,g:Aβ†’Bf, g : A \to B, then the coequaliser coeq(f,g)\mathrm{coeq}(f,g) can be thought of as β€œBB, with the images of ff and gg identified”.

data Coeq (f g : A β†’ B) : Type (level-of A βŠ” level-of B) where
  inc    : B β†’ Coeq f g
  glue   : βˆ€ x β†’ inc (f x) ≑ inc (g x)
  squash : is-set (Coeq f g)

The universal property of coequalisers, being a type of colimit, is a mapping-out property: Maps from coeq(f,g)\mathrm{coeq}(f,g) are maps out of BB, satisfying a certain property. Specifically, for a map h:Bβ†’Ch : B \to C, if we have h∘f=h∘gh \circ f = h \circ g, then the map ff factors (uniquely) through inc. The situation can be summarised with the diagram below.

We refer to this unique factoring as Coeq-rec.

Coeq-rec : βˆ€ {β„“} {C : Type β„“} {f g : A β†’ B}
      β†’ is-set C β†’ (h : B β†’ C)
      β†’ (βˆ€ x β†’ h (f x) ≑ h (g x)) β†’ Coeq f g β†’ C
Coeq-rec cset h h-coeqs (inc x) = h x
Coeq-rec cset h h-coeqs (glue x i) = h-coeqs x i
Coeq-rec cset h h-coeqs (squash x y p q i j) =
  cset (g x) (g y) (Ξ» i β†’ g (p i)) (Ξ» i β†’ g (q i)) i j
  where g = Coeq-rec cset h h-coeqs

An alternative phrasing of the desired universal property is precomposition with inc induces an equivalence between the β€œspace of maps Bβ†’CB \to C which coequalise ff and gg” and the maps coeq(f,g)β†’C\mathrm{coeq}(f,g) \to C. In this sense, inc is the universal map which coequalises ff and gg.

To construct the map above, we used Coeq-elim-prop, which has not yet been defined. It says that, to define a dependent function from Coeq to a family of propositions, it suffices to define how it acts on inc: The path constructions don’t matter.

Coeq-elim-prop : βˆ€ {β„“} {f g : A β†’ B} {C : Coeq f g β†’ Type β„“}
              β†’ (βˆ€ x β†’ is-prop (C x))
              β†’ (βˆ€ x β†’ C (inc x))
              β†’ βˆ€ x β†’ C x
Coeq-elim-prop cprop cinc (inc x) = cinc x

Since C was assumed to be a family of propositions, we automatically get the necessary coherences for glue and squash.

Coeq-elim-prop {f = f} {g = g} cprop cinc (glue x i) =
  is-prop→pathp (λ i → cprop (glue x i)) (cinc (f x)) (cinc (g x)) i
Coeq-elim-prop cprop cinc (squash x y p q i j) =
  is-prop→squarep (λ i j → cprop (squash x y p q i j))
    (Ξ» i β†’ g x) (Ξ» i β†’ g (p i)) (Ξ» i β†’ g (q i)) (Ξ» i β†’ g y) i j
  where g = Coeq-elim-prop cprop cinc

Since β€œthe space of maps h:Bβ†’Ch : B \to C which coequalise ff and gg” is a bit of a mouthful, we introduce an abbreviation: Since a colimit is defined to be a certain universal (co)cone, we call these Coeq-cones.

private
  coeq-cone : βˆ€ {β„“} (f g : A β†’ B) β†’ Type β„“ β†’ Type _
  coeq-cone {B = B} f g C = Ξ£[ h ∈ (B β†’ C) ] (h ∘ f ≑ h ∘ g)

The universal property of Coeq then says that Coeq-cone is equivalent to the maps coeq(f,g)β†’C\mathrm{coeq}(f,g) \to C, and this equivalence is given by inc, the β€œuniversal Coequalising map”.

Coeq-univ : βˆ€ {β„“} {C : Type β„“} {f g : A β†’ B}
          β†’ is-set C
          β†’ is-equiv {A = Coeq f g β†’ C} {B = coeq-cone f g C}
            (Ξ» h β†’ h ∘ inc , Ξ» i z β†’ h (glue z i))
Coeq-univ {C = C} {f = f} {g = g} cset =
  is-iso→is-equiv (iso cr' (λ x → refl) islinv)
  where
    open is-iso
    cr' : coeq-cone f g C β†’ Coeq f g β†’ C
    cr' (f , f-coeqs) = Coeq-rec cset f (happly f-coeqs)

    islinv : is-left-inverse cr' (Ξ» h β†’ h ∘ inc , Ξ» i z β†’ h (glue z i))
    islinv f = funext (Coeq-elim-prop (Ξ» x β†’ cset _ _) Ξ» x β†’ refl)

EliminationπŸ”—

Above, we defined what it means to define a dependent function (x:coeq(f,g))β†’CΒ x(x : \mathrm{coeq}(f,g)) \to C\ x when CC is a family of propositions, and what it means to define a non-dependent function coeq(f,g)β†’C\mathrm{coeq}(f,g) \to C. Now, we combine the two notions, and allow dependent elimination into families of sets:

Coeq-elim : βˆ€ {β„“} {f g : A β†’ B} {C : Coeq f g β†’ Type β„“}
          β†’ (βˆ€ x β†’ is-set (C x))
          β†’ (ci : βˆ€ x β†’ C (inc x))
          β†’ (βˆ€ x β†’ PathP (Ξ» i β†’ C (glue x i)) (ci (f x)) (ci (g x)))
          β†’ βˆ€ x β†’ C x
Coeq-elim cset ci cg (inc x) = ci x
Coeq-elim cset ci cg (glue x i) = cg x i
Coeq-elim cset ci cg (squash x y p q i j) =
  is-set→squarep (λ i j → cset (squash x y p q i j))
    (Ξ» i β†’ g x) (Ξ» i β†’ g (p i)) (Ξ» i β†’ g (q i)) (Ξ» i β†’ g y) i j
  where g = Coeq-elim cset ci cg

There is a barrage of combined eliminators, whose definitions are not very enlightening β€” you can mouse over these links to see their types: Coeq-elim-propβ‚‚ Coeq-elim-prop₃ Coeq-recβ‚‚.

{-# TERMINATING #-}
Coeq-elim-propβ‚‚ : βˆ€ {β„“} {f g : A β†’ B} {f' g' : A' β†’ B'}
                   {C : Coeq f g β†’ Coeq f' g' β†’ Type β„“}
               β†’ (βˆ€ x y β†’ is-prop (C x y))
               β†’ (βˆ€ x y β†’ C (inc x) (inc y))
               β†’ βˆ€ x y β†’ C x y
Coeq-elim-propβ‚‚ prop f (inc x) (inc y) = f x y
Coeq-elim-propβ‚‚ {f' = f'} {g'} prop f (inc x) (glue y i) =
  is-prop→pathp (λ i → prop (inc x) (glue y i)) (f x (f' y)) (f x (g' y)) i
Coeq-elim-propβ‚‚ prop f (inc x) (squash y y' p q i j) =
  is-prop→squarep (λ i j → prop (inc x) (squash y y' p q i j))
    (Ξ» i β†’ Coeq-elim-propβ‚‚ prop f (inc x) y)
    (Ξ» i β†’ Coeq-elim-propβ‚‚ prop f (inc x) (p i))
    (Ξ» i β†’ Coeq-elim-propβ‚‚ prop f (inc x) (q i))
    (Ξ» i β†’ Coeq-elim-propβ‚‚ prop f (inc x) y')
    i j
Coeq-elim-propβ‚‚ {f = f'} {g = g'} prop f (glue x i) y =
  is-prop→pathp (λ i → prop (glue x i) y)
    (Coeq-elim-propβ‚‚ prop f (inc (f' x)) y)
    (Coeq-elim-propβ‚‚ prop f (inc (g' x)) y)
    i
Coeq-elim-propβ‚‚ prop f (squash x x' p q i j) y =
  is-prop→squarep (λ i j → prop (squash x x' p q i j) y)
    (Ξ» i β†’ Coeq-elim-propβ‚‚ prop f x y)
    (Ξ» i β†’ Coeq-elim-propβ‚‚ prop f (p i) y)
    (Ξ» i β†’ Coeq-elim-propβ‚‚ prop f (q i) y)
    (Ξ» i β†’ Coeq-elim-propβ‚‚ prop f x' y)
    i j

Coeq-elim-prop₃ : βˆ€ {β„“} {f g : A β†’ B} {f' g' : A' β†’ B'} {f'' g'' : A'' β†’ B''}
                    {C : Coeq f g β†’ Coeq f' g' β†’ Coeq f'' g'' β†’ Type β„“}
               β†’ (βˆ€ x y z β†’ is-prop (C x y z))
               β†’ (βˆ€ x y z β†’ C (inc x) (inc y) (inc z))
               β†’ βˆ€ x y z β†’ C x y z
Coeq-elim-prop₃ cprop f (inc a) y z =
  Coeq-elim-propβ‚‚ (Ξ» x y β†’ Ξ -is-hlevel 1 Ξ» z β†’ cprop z x y)
    (Ξ» x y β†’ Coeq-elim-prop (Ξ» z β†’ cprop z (inc x) (inc y)) Ξ» z β†’ f z x y) y z (inc a)
Coeq-elim-prop₃ cprop f (glue x i) y z =
  Coeq-elim-propβ‚‚ (Ξ» x y β†’ Ξ -is-hlevel 1 Ξ» z β†’ cprop z x y)
    (Ξ» x y β†’ Coeq-elim-prop (Ξ» z β†’ cprop z (inc x) (inc y)) Ξ» z β†’ f z x y) y z
    (glue x i)
Coeq-elim-prop₃ cprop f (squash x x' p q i j) y z =
  is-prop→squarep (λ i j → cprop (squash x x' p q i j) y z)
    (Ξ» i β†’ Coeq-elim-prop₃ cprop f x y z)
    (Ξ» i β†’ Coeq-elim-prop₃ cprop f (p i) y z)
    (Ξ» i β†’ Coeq-elim-prop₃ cprop f (q i) y z)
    (Ξ» i β†’ Coeq-elim-prop₃ cprop f x' y z)
    i j

Coeq-recβ‚‚ : βˆ€ {β„“} {f g : A β†’ B} {f' g' : A' β†’ B'} {C : Type β„“}
          β†’ is-set C
          β†’ (ci : B β†’ B' β†’ C)
          β†’ (βˆ€ a x β†’ ci (f x) a ≑ ci (g x) a)
          β†’ (βˆ€ a x β†’ ci a (f' x) ≑ ci a (g' x))
          β†’ Coeq f g β†’ Coeq f' g' β†’ C
Coeq-recβ‚‚ cset ci r1 r2 (inc x) (inc y) = ci x y
Coeq-recβ‚‚ cset ci r1 r2 (inc x) (glue y i) = r2 x y i
Coeq-recβ‚‚ cset ci r1 r2 (inc x) (squash y z p q i j) = cset
  (Coeq-recβ‚‚ cset ci r1 r2 (inc x) y)
  (Coeq-recβ‚‚ cset ci r1 r2 (inc x) z)
  (Ξ» j β†’ Coeq-recβ‚‚ cset ci r1 r2 (inc x) (p j))
  (Ξ» j β†’ Coeq-recβ‚‚ cset ci r1 r2 (inc x) (q j))
  i j

Coeq-recβ‚‚ cset ci r1 r2 (glue x i) (inc x₁) = r1 x₁ x i
Coeq-recβ‚‚ {f = f} {g} {f'} {g'} cset ci r1 r2 (glue x i) (glue y j) =
  is-set→squarep (λ i j → cset)
    (Ξ» j β†’ r1 (f' y) x j)
    (Ξ» j β†’ r2 (f x) y j)
    (Ξ» j β†’ r2 (g x) y j)
    (Ξ» j β†’ r1 (g' y) x j)
    i j

Coeq-recβ‚‚ {f = f} {g} {f'} {g'} cset ci r1 r2 (glue x i) (squash y z p q j k) =
  is-hlevel-suc 2 cset
    (go (glue x i) y) (go (glue x i) z)
    (Ξ» j β†’ go (glue x i) (p j))
    (Ξ» j β†’ go (glue x i) (q j))
    (Ξ» i j β†’ exp i j) (Ξ» i j β†’ exp i j)
    i j k
  where
    go = Coeq-recβ‚‚ cset ci r1 r2
    exp : I β†’ I β†’ _
    exp l m = cset
      (go (glue x i) y) (go (glue x i) z)
      (Ξ» j β†’ go (glue x i) (p j))
      (Ξ» j β†’ go (glue x i) (q j))
      l m

Coeq-recβ‚‚ cset ci r1 r2 (squash x y p q i j) z =
  cset (go x z) (go y z) (Ξ» j β†’ go (p j) z) (Ξ» j β†’ go (q j) z) i j
  where go = Coeq-recβ‚‚ cset ci r1 r2

instance
  H-Level-coeq : βˆ€ {f g : A β†’ B} {n} β†’ H-Level (Coeq f g) (2 + n)
  H-Level-coeq = basic-instance 2 squash

QuotientsπŸ”—

With dependent sums, we can recover quotients as a special case of coequalisers. Observe that, by taking the total space of a relation R:A→A→TypeR : A \to A \to \mathrm{Type}, we obtain two projection maps which have as image all of the possible related elements in AA. By coequalising these projections, we obtain a space where any related objects are identified: The quotient A/RA/R.

private
  tot : βˆ€ {β„“} β†’ (A β†’ A β†’ Type β„“) β†’ Type (level-of A βŠ” β„“)
  tot {A = A} R = Σ[ x ∈ A ] Σ[ y ∈ A ] R x y

  /-left : βˆ€ {β„“} {R : A β†’ A β†’ Type β„“} β†’ tot R β†’ A
  /-left (x , _ , _) = x

  /-right : βˆ€ {β„“} {R : A β†’ A β†’ Type β„“} β†’ tot R β†’ A
  /-right (_ , x , _) = x

private variable
  R S T : A β†’ A β†’ Type β„“

We form the quotient as the aforementioned coequaliser of the two projections from the total space of RR:

_/_ : βˆ€ {β„“ β„“'} (A : Type β„“) (R : A β†’ A β†’ Type β„“') β†’ Type (β„“ βŠ” β„“')
A / R = Coeq (/-left {R = R}) /-right

quot : βˆ€ {β„“ β„“'} {A : Type β„“} {R : A β†’ A β†’ Type β„“'} {x y : A} β†’ R x y
    β†’ Path (A / R) (inc x) (inc y)
quot r = glue (_ , _ , r)

Using Coeq-elim, we can recover the elimination principle for quotients:

Quot-elim : βˆ€ {β„“} {B : A / R β†’ Type β„“}
          β†’ (βˆ€ x β†’ is-set (B x))
          β†’ (f : βˆ€ x β†’ B (inc x))
          β†’ (βˆ€ x y (r : R x y) β†’ PathP (Ξ» i β†’ B (quot r i)) (f x) (f y))
          β†’ βˆ€ x β†’ B x
Quot-elim bset f r = Coeq-elim bset f Ξ» { (x , y , w) β†’ r x y w }

EffectivityπŸ”—

The most well-behaved case of quotients is when R:A→A→TypeR : A \to A \to \mathrm{Type} takes values in propositions, is reflexive, transitive and symmetric (an equivalence relation). In this case, we have that the quotient A/RA / R is effective: The map quot is an equivalence.

record Congruence {β„“} (A : Type β„“) β„“' : Type (β„“ βŠ” lsuc β„“') where
  field
    _∼_         : A β†’ A β†’ Type β„“'
    has-is-prop : βˆ€ x y β†’ is-prop (x ∼ y)
    reflᢜ : βˆ€ {x} β†’ x ∼ x
    _βˆ™αΆœ_  : βˆ€ {x y z} β†’ x ∼ y β†’ y ∼ z β†’ x ∼ z
    symᢜ  : βˆ€ {x y}   β†’ x ∼ y β†’ y ∼ x

  relation = _∼_

  quotient : Type _
  quotient = A / _∼_

module _ {A : Type β„“} (R : Congruence A β„“') where
  private module R = Congruence R

We will show this using an encode-decode method. For each x:Ax : A, we define a type family Codex(p)\mathrm{Code}_x(p), which represents an equality inc(x)=y\mathrm{inc}(x) = y. Importantly, the fibre over inc(y)\mathrm{inc}(y) will be R(x,y)R(x, y), so that the existence of functions converting between Codex(y)\mathrm{Code}_x(y) and paths inc(x)=y\mathrm{inc}(x) = y is enough to establish effectivity of the quotient.

  private
    Code : A β†’ R.quotient β†’ Prop β„“'
    Code x = Quot-elim
      (Ξ» x β†’ n-Type-is-hlevel 1)
      (Ξ» y β†’ el (x R.∼ y) (R.has-is-prop x y) {- 1 -})
      Ξ» y z r β†’
        n-ua (prop-ext (R.has-is-prop _ _) (R.has-is-prop _ _)
          (Ξ» z β†’ z R.βˆ™αΆœ r)
          Ξ» z β†’ z R.βˆ™αΆœ (R.symᢜ r))

We do quotient induction into the type of propositions, which by univalence is a set. Since the fibre over inc(y)\mathrm{inc}(y) must be R(x,y)R(x, y), that’s what we give for the inc constructor ({- 1 -}, above). For this to respect the quotient, it suffices to show that, given R(y,z)R(y,z), we have R(x,y)⇔R(x,z)R(x,y) \Leftrightarrow R(x,z), which follows from the assumption that RR is an equivalence relation ({- 2 -}).

    encode : βˆ€ x y (p : inc x ≑ y) β†’ ∣ Code x y ∣
    encode x y p = subst (Ξ» y β†’ ∣ Code x y ∣) p R.reflᢜ

    decode : βˆ€ x y (p : ∣ Code x y ∣) β†’ inc x ≑ y
    decode x y p =
      Coeq-elim-prop {C = Ξ» y β†’ (p : ∣ Code x y ∣) β†’ inc x ≑ y}
        (Ξ» _ β†’ Ξ -is-hlevel 1 Ξ» _ β†’ squash _ _) (Ξ» y r β†’ quot r) y p

For encode, it suffices to transport the proof that RR is reflexive along the given proof, and for decoding, we eliminate from the quotient to a proposition. It boils down to establishing that R(x,y)β†’inc(x)≑inc(y)R(x,y) \to \mathrm{inc}(x) \equiv \mathrm{inc}(y), which is what the constructor quot says. Putting this all together, we get a proof that equivalence relations are effective.

  effective : βˆ€ {x y : A} β†’ is-equiv (quot {R = R.relation})
  effective {x = x} {y} =
    prop-ext (R.has-is-prop x y) (squash _ _) (decode x (inc y)) (encode x (inc y)) .snd

Quot-opβ‚‚ : βˆ€ {C : Type β„“} {T : C β†’ C β†’ Type β„“'}
         β†’ (βˆ€ x β†’ R x x) β†’ (βˆ€ y β†’ S y y)
         β†’ (_⋆_ : A β†’ B β†’ C)
         β†’ ((a b : A) (x y : B) β†’ R a b β†’ S x y β†’ T (a ⋆ x) (b ⋆ y))
         β†’ A / R β†’ B / S β†’ C / T
Quot-opβ‚‚ Rr Sr op resp =
  Coeq-recβ‚‚ squash (Ξ» x y β†’ inc (op x y))
    (Ξ» { z (x , y , r) β†’ quot (resp x y z z r (Sr z)) })
    Ξ» { z (x , y , r) β†’ quot (resp z z x y (Rr z) r) }

Discrete-quotient
  : βˆ€ {A : Type β„“} (R : Congruence A β„“')
  β†’ (βˆ€ x y β†’ Dec (Congruence.relation R x y))
  β†’ Discrete (Congruence.quotient R)
Discrete-quotient cong rdec =
  Coeq-elim-propβ‚‚ {C = Ξ» x y β†’ Dec (x ≑ y)} (Ξ» x y β†’ hlevel 1) go _ _ where
  go : βˆ€ x y β†’ Dec (inc x ≑ inc y)
  go x y with rdec x y
  ... | yes xRy = yes (quot xRy)
  ... | no ¬xRy = no λ p → ¬xRy (equiv→inverse (effective cong) p)