open import 1Lab.Reflection.Induction
open import 1Lab.Reflection using (_v∷_ ; typeError)
open import 1Lab.Prelude

open import Data.List.Base
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 then the coequaliser can be thought of as β€œ with the images of and 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 are maps out of satisfying a certain property. Specifically, for a map if we have then the map 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} ⦃ _ : H-Level C 2 ⦄
  β†’ (h : B β†’ C)
  β†’ (βˆ€ x β†’ h (f x) ≑ h (g x)) β†’ Coeq f g β†’ C
Coeq-rec h h-coeqs (inc x) = h x
Coeq-rec h h-coeqs (glue x i) = h-coeqs x i
Coeq-rec ⦃ cs ⦄ h h-coeqs (squash x y p q i j) =
  hlevel 2 (g x) (g y) (Ξ» i β†’ g (p i)) (Ξ» i β†’ g (q i)) i j
  where g = Coeq-rec ⦃ cs ⦄ h h-coeqs

An alternative phrasing of the desired universal property is precomposition with inc induces an equivalence between the β€œspace of maps which coequalise and ” and the maps In this sense, inc is the universal map which coequalises and

This is hella confusing, because we need coeq-elim-prop to define Coeq-univ, but Coeq-univ comes first in the β€œdidactic order”!

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
instance
  Inductive-Coeq
    : βˆ€ {β„“ β„“m} {f g : A β†’ B} {P : Coeq f g β†’ Type β„“}
    β†’ ⦃ _ : Inductive (βˆ€ x β†’ P (inc x)) β„“m ⦄
    β†’ ⦃ _ : βˆ€ {x} β†’ H-Level (P x) 1 ⦄
    β†’ Inductive (βˆ€ x β†’ P x) β„“m
  Inductive-Coeq ⦃ i ⦄ = record
    { methods = i .Inductive.methods
    ; from    = Ξ» f β†’ Coeq-elim-prop (Ξ» x β†’ hlevel 1) (i .Inductive.from f)
    }

  Extensional-coeq-map
    : βˆ€ {β„“ β„“' β„“'' β„“r} {A : Type β„“} {B : Type β„“'} {C : Type β„“''} {f g : A β†’ B}
    β†’ ⦃ sf : Extensional (B β†’ C) β„“r ⦄ ⦃ _ : H-Level C 2 ⦄
    β†’ Extensional (Coeq f g β†’ C) β„“r
  Extensional-coeq-map ⦃ sf ⦄ .Pathᡉ f g = sf .Pathᡉ (f ∘ inc) (g ∘ inc)
  Extensional-coeq-map ⦃ sf ⦄ .reflᡉ f = sf .reflᡉ (f ∘ inc)
  Extensional-coeq-map ⦃ sf ⦄ .idsᡉ .to-path h = funext $
    elim! (happly (sf .idsᡉ .to-path h))
  Extensional-coeq-map ⦃ sf ⦄ .idsᡉ .to-path-over p =
    is-propβ†’pathp (Ξ» i β†’ Pathᡉ-is-hlevel 1 sf (hlevel 2)) _ _

  Number-Coeq : βˆ€ {β„“ β„“'} {A : Type β„“} {B : Type β„“'} β†’ ⦃ Number B ⦄ β†’ {f g : A β†’ B} β†’ Number (Coeq f g)
  Number-Coeq {β„“ = β„“} ⦃ b ⦄ .Number.Constraint n = Lift β„“ (b .Number.Constraint n)
  Number-Coeq ⦃ b ⦄ .Number.fromNat n ⦃ lift c ⦄ = inc (b .Number.fromNat n ⦃ c ⦄)

Since β€œthe space of maps which coequalise and ” 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 and this equivalence is given by inc, the β€œuniversal Coequalising map”.

Coeq-univ : βˆ€ {β„“} {C : Type β„“} {f g : A β†’ B} ⦃ _ : H-Level C 2 ⦄
          β†’ 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} =
  is-iso→is-equiv (iso cr' (λ x → refl) islinv) where
    cr' : coeq-cone f g C β†’ Coeq f g β†’ C
    cr' (f , f-coeqs) = Coeq-rec f (happly f-coeqs)

    islinv : is-left-inverse cr' (Ξ» h β†’ h ∘ inc , Ξ» i z β†’ h (glue z i))
    islinv f = ext Ξ» _ β†’ refl

EliminationπŸ”—

Above, we defined what it means to define a dependent function when is a family of propositions, and what it means to define a non-dependent function 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
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 we obtain two projection maps which have as image all of the possible related elements in By coequalising these projections, we obtain a space where any related objects are identified: the quotient 

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 

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

infixl 25 _/_

quot : βˆ€ {β„“ β„“'} {A : Type β„“} {R : A β†’ A β†’ Type β„“'} {x y : A} β†’ R x y
    β†’ Path (A / R) (inc x) (inc y)
quot r = glue (_ , _ , r)
{-# DISPLAY Coeq (/-left {_} {A} {_} {R}) /-right = A / 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 }

Conversely, we can describe coequalisers in terms of quotients. In order to form the coequaliser of we interpret the span formed by and as a binary relation on a witness that are related is an element of the fibre of at that is an such that and 

span→R
  : βˆ€ {β„“ β„“'} {A : Type β„“} {B : Type β„“'} (f g : A β†’ B)
  β†’ B β†’ B β†’ Type (β„“ βŠ” β„“')
spanβ†’R f g = curry (fibre ⟨ f , g ⟩)

We then recover the coequaliser of and as the quotient of by this relation.

Coeq≃quotient
  : βˆ€ {β„“ β„“'} {A : Type β„“} {B : Type β„“'} (f g : A β†’ B)
  β†’ Coeq f g ≃ B / spanβ†’R f g
Coeq≃quotient f g .fst = Coeq-rec inc Ξ» a β†’ quot (a , refl)
Coeq≃quotient f g .snd = is-isoβ†’is-equiv Ξ» where
  .is-iso.from β†’ Coeq-rec inc Ξ» (_ , _ , a , p) β†’
    sym (ap (inc ∘ fst) p) βˆ™βˆ™ glue a βˆ™βˆ™ ap (inc ∘ snd) p
  .is-iso.rinv β†’ elim! Ξ» _ β†’ refl
  .is-iso.linv β†’ elim! Ξ» _ β†’ refl
inc-is-surjective : {f g : A β†’ B} β†’ is-surjective {B = Coeq f g} inc
inc-is-surjective (inc x) = inc (x , refl)
inc-is-surjective {f = f} {g = g} (glue x i) = is-prop→pathp
  (Ξ» i β†’ βˆ₯_βˆ₯.squash {A = fibre Coeq.inc (glue x i)})
  (βˆ₯_βˆ₯.inc (f x , refl))
  (βˆ₯_βˆ₯.inc (g x , refl)) i
inc-is-surjective (squash x y p q i j) = is-prop→squarep
  (Ξ» i j β†’ βˆ₯_βˆ₯.squash {A = fibre inc (squash x y p q i j)})
  (Ξ» i β†’ inc-is-surjective x)
  (Ξ» j β†’ inc-is-surjective (p j))
  (Ξ» j β†’ inc-is-surjective (q j))
  (Ξ» i β†’ inc-is-surjective y) i j

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) }

EffectivityπŸ”—

The most well-behaved case of quotients is when takes values in propositions, is reflexive, transitive and symmetric (an equivalence relation). In this case, we have that the quotient 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

  infixr 30 _βˆ™αΆœ_

  relation = _∼_

  quotient : Type _
  quotient = A / _∼_

We will show this using an encode-decode method. For each we define a type family which represents an equality Importantly, the fibre over will be so that the existence of functions converting between and paths 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 must be that’s what we give for the inc constructor ({- 1 -}, above). For this to respect the quotient, it suffices to show that, given we have which follows from the assumption that 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 = elim! Ξ» x y r β†’ quot r

For encode, it suffices to transport the proof that is reflexive along the given proof, and for decoding, we eliminate from the quotient to a proposition. It boils down to establishing that 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
  effective : βˆ€ {x y : A} β†’ Path quotient (inc x) (inc y) β†’ x ∼ y
  effective = equiv→inverse is-effective

  reflᢜ' : βˆ€ {x y : A} β†’ x ≑ y β†’ x ∼ y
  reflᢜ' {x = x} p = transport (Ξ» i β†’ x ∼ p i) reflᢜ

  opβ‚‚
    : (f : A β†’ A β†’ A)
    β†’ (βˆ€ x y u v β†’ x ∼ u β†’ y ∼ v β†’ f x y ∼ f u v)
    β†’ quotient β†’ quotient β†’ quotient
  opβ‚‚ f r = Quot-opβ‚‚ (Ξ» x β†’ reflᢜ) (Ξ» x β†’ reflᢜ) f (Ξ» a b x y β†’ r a x b y)

  opβ‚‚-comm
    : (f : A β†’ A β†’ A)
    β†’ (βˆ€ a b β†’ f a b ∼ f b a)
    β†’ (βˆ€ x u v β†’ u ∼ v β†’ f x u ∼ f x v)
    β†’ quotient β†’ quotient β†’ quotient
  opβ‚‚-comm f c r = opβ‚‚ f (Ξ» x y u v p q β†’ r x y v q βˆ™αΆœ c x v βˆ™αΆœ r v x u p βˆ™αΆœ c v u)
Discrete-quotient
  : βˆ€ {A : Type β„“} (R : Congruence A β„“')
  β†’ (βˆ€ x y β†’ Dec (Congruence.relation R x y))
  β†’ Discrete (Congruence.quotient R)
Discrete-quotient cong rdec .decide = elim! 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 (Congruence.effective cong p)

open hlevel-projection
private
  sim-prop : βˆ€ (R : Congruence A β„“) {x y} β†’ is-prop (R .Congruence._∼_ x y)
  sim-prop R = R .Congruence.has-is-prop _ _

instance
  hlevel-proj-congr : hlevel-projection (quote Congruence._∼_)
  hlevel-proj-congr .has-level = quote sim-prop
  hlevel-proj-congr .get-level _ = pure (quoteTerm (suc zero))
  hlevel-proj-congr .get-argument (_ ∷ _ ∷ _ ∷ c v∷ _) = pure c
  {-# CATCHALL #-}
  hlevel-proj-congr .get-argument _ = typeError []

private unquoteDecl eqv = declare-record-iso eqv (quote Congruence)
module _ {R R' : Congruence A β„“} (p : βˆ€ x y β†’ Congruence._∼_ R x y ≃ Congruence._∼_ R' x y) where
  private
    module R = Congruence R
    module R' = Congruence R'

  open Congruence

  private
    lemma : βˆ€ {x y} i β†’ is-prop (ua (p x y) i)
    lemma {x} {y} i = is-prop→pathp (λ i → is-prop-is-prop {A = ua (p x y) i}) (R.has-is-prop x y) (R'.has-is-prop x y) i

  Congruence-path : R ≑ R'
  Congruence-path i ._∼_ x y = ua (p x y) i
  Congruence-path i .has-is-prop x y = lemma i
  Congruence-path i .reflᢜ = is-propβ†’pathp lemma R.reflᢜ R'.reflᢜ i
  Congruence-path i ._βˆ™αΆœ_ = is-propβ†’pathp (Ξ» i β†’ Ξ -is-hlevelΒ² {A = ua (p _ _) i} {B = Ξ» _ β†’ ua (p _ _) i} 1 Ξ» _ _ β†’ lemma i) R._βˆ™αΆœ_ R'._βˆ™αΆœ_ i
  Congruence-path i .symᢜ = is-propβ†’pathp (Ξ» i β†’ Ξ -is-hlevel {A = ua (p _ _) i} 1 Ξ» _ β†’ lemma i) R.symᢜ R'.symᢜ i

open Congruence

Congruence-pullback
  : βˆ€ {β„“a β„“b β„“} {A : Type β„“a} {B : Type β„“b}
  β†’ (A β†’ B) β†’ Congruence B β„“ β†’ Congruence A β„“
Congruence-pullback {β„“ = β„“} {A = A} f R = f*R where
  module R = Congruence R
  f*R : Congruence A β„“
  f*R ._∼_ x y = f x R.∼ f y
  f*R .has-is-prop x y = R.has-is-prop _ _
  f*R .reflᢜ = R.reflᢜ
  f*R ._βˆ™αΆœ_ f g = f R.βˆ™αΆœ g
  f*R .symᢜ f = R.symᢜ f

Relation to surjectionsπŸ”—

As mentioned in the definition of surjection, we can view a cover as expressing a way of gluing together the type by adding paths between the elements of When and 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 the congruence on defined to be identity under 

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 is a surjection into a set, then is the quotient of under the kernel pair of 

surjection→is-quotient
  : βˆ€ {β„“ β„“'} {A : Type β„“} {B : Type β„“'}
  β†’ (b-set : is-set B)
  β†’ (f : A β†  B)
  β†’ B ≃ Congruence.quotient (Kernel-pair b-set (f .fst))
surjection→is-quotient {A = A} {B} b-set (f , surj) =
  _ , injective-surjective→is-equiv! g'-inj g'-surj
  where

  module c = Congruence (Kernel-pair b-set f)

The construction is pretty straightforward: each fibre defines an element If we have another fibre then because

so the function is constant, and factors through the propositional truncation 

  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 2) gβ‚€ gβ‚€-const f

Since each is inhabited, all of these functions glue together to give a function 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)
private module test where
  variable C : Type β„“

  _ : {f g : A / R β†’ B} ⦃ _ : H-Level B 2 ⦄
    β†’ ((x : A) β†’ f (inc x) ≑ g (inc x)) β†’ f ≑ g
  _ = ext

  _ : {f g : (A Γ— B) / R β†’ C} ⦃ _ : H-Level C 2 ⦄
    β†’ ((x : A) (y : B) β†’ f (inc (x , y)) ≑ g (inc (x , y)))
    β†’ f ≑ g
  _ = ext

ClosuresπŸ”—

We define the reflexive, transitive and symmetric closure of a relation and prove that it induces the same quotient as 

module _ {β„“ β„“'} {A : Type β„“} (R : A β†’ A β†’ Type β„“') where
  data Closure : A β†’ A β†’ Type (β„“ βŠ” β„“') where
    inc : βˆ€ {x y} β†’ R x y β†’ Closure x y
    Closure-refl : βˆ€ {x} β†’ Closure x x
    Closure-trans : βˆ€ {x y z} β†’ Closure x y β†’ Closure y z β†’ Closure x z
    Closure-sym : βˆ€ {x y} β†’ Closure y x β†’ Closure x y
    squash : βˆ€ {x y} β†’ is-prop (Closure x y)

  Closure-congruence : Congruence A _
  Closure-congruence .Congruence._∼_ = Closure
  Closure-congruence .Congruence.has-is-prop _ _ = squash
  Closure-congruence .Congruence.reflᢜ = Closure-refl
  Closure-congruence .Congruence._βˆ™αΆœ_ = Closure-trans
  Closure-congruence .Congruence.symᢜ = Closure-sym
  unquoteDecl Closure-elim-prop = make-elim-n 1 Closure-elim-prop (quote Closure)

  Closure-rec-congruence
    : βˆ€ {β„“''} (S : Congruence A β„“'') (let module S = Congruence S)
    β†’ (βˆ€ {x y} β†’ R x y β†’ x S.∼ y)
    β†’ βˆ€ {x y} β†’ Closure x y β†’ x S.∼ y
  Closure-rec-congruence S h = Closure-elim-prop
    {P = Ξ» {x} {y} _ β†’ x S.∼ y}
    (Ξ» _ β†’ S.has-is-prop _ _)
    h S.reflᢜ (Ξ» _ q _ r β†’ q S.βˆ™αΆœ r) (Ξ» _ r β†’ S.symᢜ r)
    where module S = Congruence S

  Closure-rec-≑
    : βˆ€ {β„“'} {D : Type β„“'}
    β†’ ⦃ H-Level D 2 ⦄
    β†’ (f : A β†’ D)
    β†’ (βˆ€ {x y} β†’ R x y β†’ f x ≑ f y)
    β†’ βˆ€ {x y} β†’ Closure x y β†’ f x ≑ f y
  Closure-rec-≑ f = Closure-rec-congruence (Kernel-pair (hlevel 2) f)
Closure-quotient
  : βˆ€ {β„“ β„“'} {A : Type β„“} (R : A β†’ A β†’ Type β„“')
  β†’ A / R ≃ A / Closure R
Closure-quotient {A = A} R .fst = Coeq-rec inc Ξ» (a , b , r) β†’ quot (inc r)
Closure-quotient {A = A} R .snd = is-iso→is-equiv λ where
  .is-iso.from β†’ Coeq-rec inc Ξ» (a , b , r) β†’ Closure-rec-≑ _ inc quot r
  .is-iso.rinv β†’ elim! Ξ» _ β†’ refl
  .is-iso.linv β†’ elim! Ξ» _ β†’ refl
instance
  Closure-H-Level
    : βˆ€ {β„“ β„“'} {A : Type β„“} {R : A β†’ A β†’ Type β„“'} {x y} {n}
    β†’ H-Level (Closure R x y) (suc n)
  Closure-H-Level = prop-instance squash

Coeq-ap
  : βˆ€ {β„“a β„“a' β„“b β„“b'} {A : Type β„“a} {A' : Type β„“a'} {B : Type β„“b} {B' : Type β„“b'}
      {f g : A β†’ B} {f' g' : A' β†’ B'} (ea : A ≃ A') (eb : B ≃ B')
  β†’ (p : f' ≑ Equiv.to eb ∘ f ∘ Equiv.from ea) (q : g' ≑ Equiv.to eb ∘ g ∘ Equiv.from ea)
  β†’ Coeq f g ≃ Coeq f' g'
Coeq-ap {f = f} {g} {f'} {g'} ea eb p q = to , to-is where
  module ea = Equiv ea
  module eb = Equiv eb

  to : Coeq f g β†’ Coeq f' g'
  to (inc x) = inc (eb.to x)
  to (glue x i) = along i $
    inc (eb.to (f x))  β‰‘Λ˜βŸ¨ ap Coeq.inc (happly p (ea.to x) βˆ™ ap eb.to (ap f (ea.Ξ· x))) ⟩
    inc (f' (ea.to x)) β‰‘βŸ¨ Coeq.glue {f = f'} {g'} (ea.to x) ⟩
    inc (g' (ea.to x)) β‰‘βŸ¨ ap Coeq.inc (happly q (ea.to x) βˆ™ ap eb.to (ap g (ea.Ξ· x))) ⟩
    inc (eb.to (g x))  ∎
  to (squash x y p q i j) = squash (to x) (to y) (Ξ» i β†’ to (p i)) (Ξ» i β†’ to (q i)) i j

  from : Coeq f' g' β†’ Coeq f g
  from (inc x) = inc (eb.from x)
  from (glue x i) = along i $
    inc (eb.from (f' x)) β‰‘βŸ¨ ap Coeq.inc (eb.injective (eb.Ξ΅ _ βˆ™ happly p x)) ⟩
    inc (f (ea.from x))  β‰‘βŸ¨ Coeq.glue (ea.from x) ⟩
    inc (g (ea.from x))  β‰‘βŸ¨ ap Coeq.inc (eb.injective (sym (happly q x) βˆ™ sym (eb.Ξ΅ _))) ⟩
    inc (eb.from (g' x)) ∎
  from (squash x y p q i j) = squash (from x) (from y) (Ξ» i β†’ from (p i)) (Ξ» i β†’ from (q i)) i j

  li : from ∘ to ≑ Ξ» x β†’ x
  li = ext Ξ» x β†’ ap inc (eb.Ξ· _)

  ri : to ∘ from ≑ Ξ» x β†’ x
  ri = ext Ξ» x β†’ ap inc (eb.Ξ΅ _)

  to-is : is-equiv to
  to-is = is-iso→is-equiv (iso from (happly ri) (happly li))