module Data.Set.Coequaliser where

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 \to B$, then the coequaliser $\mathrm{coeq}(f,g)$ can be thought of as “$B$, with the images of $f$ and $g$ 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 $\mathrm{coeq}(f,g)$ are maps out of $B$, satisfying a certain property. Specifically, for a map $h : B \to C$, if we have $h \circ f = h \circ g$, then the map $f$ 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 \to C$ which coequalise $f$ and $g$” and the maps $\mathrm{coeq}(f,g) \to C$. In this sense, inc is the universal map which coequalises $f$ and $g$.

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

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

private
  coeq-cone : ∀ {ℓ} (f g : A → B) → Type ℓ → Type _
  coeq-cone {B = B} f g C = Σ[ h ∈ (B → C) ] (h ∘ f ≡ h ∘ g)

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 : \mathrm{coeq}(f,g)) \to C\ x$ when $C$ is a family of propositions, and what it means to define a non-dependent function $\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₂.

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 \to A \to \mathrm{Type}$, we obtain two projection maps which have as image all of the possible related elements in $A$. By coequalising these projections, we obtain a space where any related objects are identified: The quotient $A/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

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

_/_ : ∀ {ℓ ℓ'} (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 \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 / 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 / _∼_

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

  private
    Code : A → quotient → Prop ℓ'
    Code x = Quot-elim
      (λ x → n-Type-is-hlevel 1)
      (λ y → el (x ∼ y) (has-is-prop x y) {- 1 -})
      λ y z r →
        n-ua (prop-ext (has-is-prop _ _) (has-is-prop _ _)
          (λ z → z ∙ᶜ r)
          λ z → z ∙ᶜ (symᶜ r))

We do quotient induction into the type of propositions, which by univalence is a set. Since the fibre over $\mathrm{inc}(y)$ must be $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)$, we have $R(x,y) \Leftrightarrow R(x,z)$, which follows from the assumption that $R$ 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 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 $R$ 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) \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.

  is-effective : ∀ {x y : A} → is-equiv (quot {R = relation})
  is-effective {x = x} {y} =
    prop-ext (has-is-prop x y) (squash _ _) (decode x (inc y)) (encode x (inc y)) .snd

Relation to surjections🔗

As mentioned in the definition of surjection, we can view a cover $f : A \to B$ as expressing a way of gluing together the type $B$ by adding paths between the elements of $A$. When $A$ and $B$ are sets, this sounds a lot like a quotient! And, indeed, we can prove that every surjection induces an equivalence between its codomain and a quotient of its domain.

First, we define the kernel pair of a function $f : A \to B$, the congruence on $A$ defined to be identity under $f$.

Kernel-pair
  : ∀ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'} → is-set B → (A → B)
  → Congruence A ℓ'
Kernel-pair b-set f ._∼_ a b = f a ≡ f b
Kernel-pair b-set f .has-is-prop x y = b-set (f x) (f y)
Kernel-pair b-set f .reflᶜ = refl
Kernel-pair b-set f ._∙ᶜ_  = _∙_
Kernel-pair b-set f .symᶜ  = sym

We can then set about proving that, if $f : A \twoheadrightarrow B$ is a surjection into a set, then $B$ is the quotient of $A$ under the kernel pair of $f$.

The construction is pretty straightforward: each fibre $(a, p) : f^*x$ defines an element $[a] : A/\ker f$; If we have another fibre $(b, q)$, then $[a] = [b]$ because

$$f(a) \overset{p}{\equiv} x \overset{q}{\equiv} f(b) \text{,}$$

so the function $f^*x \to A/\ker f$ is constant, and factors through the propositional truncation $\| f^*x \|$.

  g₀ : ∀ {x} → fibre f x → c.quotient
  g₀ (a , p) = inc a

  abstract
    g₀-const : ∀ {x} (p₁ p₂ : fibre f x) → g₀ p₁ ≡ g₀ p₂
    g₀-const (_ , p) (_ , q) = quot (p ∙ sym q)

  g₁ : ∀ {x} → ∥ fibre f x ∥ → c.quotient
  g₁ f = ∥-∥-rec-set hlevel! g₀ g₀-const f

Since each $\| f^*x \|$ is inhabited, all of these functions glue together to give a function $B \to A/\ker f$. A simple calculation shows that this function is both injective and surjective; since its codomain is a set, that means it’s an equivalence.

  g' : B → c.quotient
  g' x = g₁ (surj x)

  g'-inj : injective g'
  g'-inj {x} {y} = ∥-∥-elim₂ {P = λ a b → g₁ a ≡ g₁ b → x ≡ y}
    (λ _ _ → fun-is-hlevel 1 (b-set _ _))
    (λ (_ , p) (_ , q) r → sym p ∙ c.effective r ∙ q)
    (surj x) (surj y)

  g'-surj : is-surjective g'
  g'-surj x = do
    (y , p) ← inc-is-surjective x
    pure (f y , ap g₁ (squash (surj (f y)) (inc (y , refl))) ∙ p)