Suggestion: provide proof that set-coequalizers of finite sets are finite?

[finegeometer]

I recently found myself in need of a theorem that any set-coequalizer of finite sets is finite. Would it make sense to add this theorem to the standard library, either in Cubical.Data.FinSet.Constructors or in Cubical.HITs.SetCoequalizer.Properties?

For reference, here's the proof I eventually managed to construct. This code would need some work to bring it up to the standards of this library, but it at least demonstrates that the theorem is correct, along with one possible method of proving it. (I'd be curious to know if there's a shorter proof!)

{-# OPTIONS --cubical --safe #-}

-- Theorem: A set-coequalizer of finite sets is finite.
module FinCoeq where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Equiv using (_≃_)
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Isomorphism using (isoToEquiv; iso)
open import Cubical.Foundations.Structure using (⟨_⟩; str)
open import Cubical.Foundations.Function using (case_of_; case_return_of_)
open import Cubical.Data.FinSet as FinSet using (FinSet; isFinSet)
open import Cubical.Data.FinSet.Induction
open import Cubical.Data.FinSet.Constructors
open import Cubical.Relation.Nullary

import Cubical.Data.Empty as ⊥
import Cubical.Data.Unit as ⊤
import Cubical.Data.Sum as ⊎
import Cubical.Data.Sigma as Σ
import Cubical.HITs.SetCoequalizer as SetCoeq

abstract
  private
    -- The coequalizer of the unique functions `0 → X` is X.
    Coeq0 : ∀ (X : FinSet ℓ-zero) (f g : ⟨ 𝟘 {ℓ-zero} ⟩ → ⟨ X ⟩) → ⟨ X ⟩ ≃ SetCoeq.SetCoequalizer f g
    Coeq0 X f g = isoToEquiv
      (iso
        SetCoeq.inc
        (SetCoeq.rec (FinSet.isFinSet→isSet (str X)) (λ x → x) λ ())
        (SetCoeq.elimProp (λ _ → SetCoeq.squash _ _) (λ _ → refl))
        (λ b → refl))

    -- I define an eliminator into sets for set-coequalizers, since it seems to be missing from the standard library.
    module _ {A B : Type} {f g : A → B} {C : SetCoeq.SetCoequalizer f g → Type}
      (Cset : ∀ s → isSet (C s))
      (h : (b : B) → C (SetCoeq.inc b))
      (hcoeqs : (a : A) → PathP (λ i → C (SetCoeq.coeq a i)) (h (f a)) (h (g a))) where

      CoeqElim : (s : SetCoeq.SetCoequalizer f g) → C s
      CoeqElim (SetCoeq.inc x) = h x
      CoeqElim (SetCoeq.coeq a i) = hcoeqs a i
      CoeqElim (SetCoeq.squash s t p q i j) =
        isOfHLevel→isOfHLevelDep 2 Cset (CoeqElim s) (CoeqElim t) (cong CoeqElim p) (cong CoeqElim q) (SetCoeq.squash s t p q) i j

    module Merge (X : FinSet ℓ-zero) {left right : ⟨ X ⟩} (l≠r : ¬ (left ≡ right)) where
      Merge : FinSet ℓ-zero
      Merge = _ , isFinSetΣ X (λ x → _ , (isFinSet¬ (_ , isFinSet≡ X x left)))

      testFn : (x : ⟨ X ⟩) → Dec (x ≡ left)
      testFn x = FinSet.isFinSet→Discrete (str X) x left

      testFn-left : testFn left ≡ yes refl
      testFn-left = case testFn left return _≡ yes refl of λ
        { (yes eq) → cong yes (FinSet.isFinSet→isSet (str X) left left eq refl)
        ; (no pf) → ⊥.rec (pf refl)
        }

      testFn-notLeft : ∀ {x} (pf : ¬ (x ≡ left)) → testFn x ≡ no pf
      testFn-notLeft {x} pf = case testFn x return _≡ no pf of λ
        { (yes eq) → ⊥.rec (pf eq)
        ; (no pf') → cong no (isProp¬ (x ≡ left) pf' pf)
        }

      handler : {x : ⟨ X ⟩} → Dec (x ≡ left) → ⟨ Merge ⟩
      handler {x} d = 
        case d of λ
          { (yes _) → right , λ eq → l≠r (sym eq)
          ; (no pf) → x , pf
          }

      toMerge : ⟨ X ⟩ → ⟨ Merge ⟩
      toMerge x = handler (testFn x)

      toMerge-left : fst (toMerge left) ≡ right
      toMerge-left = subst (λ d → fst (handler d) ≡ right) (sym testFn-left) refl

      toMerge-notLeft : ∀ {x} → ¬ (x ≡ left) → fst (toMerge x) ≡ x
      toMerge-notLeft {x} neq = subst (λ d → fst (handler d) ≡ x) (sym (testFn-notLeft neq)) refl

      toMerge-merge : toMerge left ≡ toMerge right
      toMerge-merge = Σ.Σ≡Prop (λ x → isProp¬ (x ≡ left)) (toMerge-left ∙ sym (toMerge-notLeft (λ eq → l≠r (sym eq))))

  -- The main theorem.
  isFinSetCoeq : ∀ {A B : FinSet ℓ-zero} (f g : ⟨ A ⟩ → ⟨ B ⟩) → isFinSet (SetCoeq.SetCoequalizer f g)
  isFinSetCoeq {A} {B} = elimProp𝟙+
    (λ A → ∀ (B : FinSet ℓ-zero) (f g : ⟨ A ⟩ → ⟨ B ⟩) → isFinSet (SetCoeq.SetCoequalizer f g))
    (λ _ → isPropΠ3 λ _ _ _ → FinSet.isPropIsFinSet)
    (λ B f g → FinSet.EquivPresIsFinSet (Coeq0 B f g) (str B))
    (λ {A} IH B f g →
      let
        Previous : FinSet ℓ-zero
        Previous = _ , IH B (λ a → f (⊎.inr a)) (λ a → g (⊎.inr a))

        redundant : Dec (Path ⟨ Previous ⟩ (SetCoeq.inc (f (⊎.inl ⊤.tt*))) (SetCoeq.inc (g (⊎.inl ⊤.tt*))))
        redundant = FinSet.isFinSet→Discrete (str Previous) _ _
      in case redundant of λ
        { (yes pf) →
          let
            fwd : ⟨ Previous ⟩ → SetCoeq.SetCoequalizer f g
            fwd = SetCoeq.rec SetCoeq.squash SetCoeq.inc (λ a → SetCoeq.coeq (⊎.inr a))

            bwd : SetCoeq.SetCoequalizer f g → ⟨ Previous ⟩
            bwd = SetCoeq.rec SetCoeq.squash SetCoeq.inc (λ {(⊎.inl tt*) → pf; (⊎.inr a) → SetCoeq.coeq a})

            fwd-bwd : ∀ x → fwd (bwd x) ≡ x
            fwd-bwd = CoeqElim (λ _ → isSet→isGroupoid SetCoeq.squash _ _) (λ _ → refl)
              (λ _ → toPathP (SetCoeq.squash _ _ _ _))

            bwd-fwd : ∀ x → bwd (fwd x) ≡ x
            bwd-fwd = CoeqElim (λ _ → isSet→isGroupoid SetCoeq.squash _ _) (λ _ → refl)
              (λ _ → toPathP (SetCoeq.squash _ _ _ _))

            same-as-previous : ⟨ Previous ⟩ ≃ SetCoeq.SetCoequalizer f g
            same-as-previous = isoToEquiv (iso fwd bwd fwd-bwd bwd-fwd)
          in FinSet.EquivPresIsFinSet same-as-previous (str Previous)
        ; (no pf) →
          let
            open Merge Previous pf

            weaken-coequalizer : ∀ b₁ b₂ →
              Path (SetCoeq.SetCoequalizer (λ a → f (⊎.inr a)) (λ a → g (⊎.inr a)))
                (SetCoeq.inc b₁) (SetCoeq.inc b₂) →
              Path (SetCoeq.SetCoequalizer f g)
                (SetCoeq.inc b₁) (SetCoeq.inc b₂)
            weaken-coequalizer b₁ b₂ eq i = CoeqElim (λ _ → SetCoeq.squash) SetCoeq.inc (λ a → SetCoeq.coeq (⊎.inr a)) (eq i)

            fwd : ⟨ Merge ⟩ → SetCoeq.SetCoequalizer f g
            fwd = λ (x , _) → SetCoeq.rec SetCoeq.squash SetCoeq.inc (λ a → SetCoeq.coeq (⊎.inr a)) x

            bwd : SetCoeq.SetCoequalizer f g → ⟨ Merge ⟩
            bwd = SetCoeq.rec
              (FinSet.isFinSet→isSet (str Merge))
              (λ b → toMerge (SetCoeq.inc b))
              λ {(⊎.inl tt*) → toMerge-merge; (⊎.inr a) → cong toMerge (SetCoeq.coeq a)}

            fwd-bwd : ∀ x → fwd (bwd x) ≡ x
            fwd-bwd = CoeqElim
              (λ _ → isSet→isGroupoid SetCoeq.squash _ _)
              (λ b → case (testFn (SetCoeq.inc b)) return (λ d → fwd (handler d) ≡ SetCoeq.inc b) of λ
                { (yes eq) →
                  sym (weaken-coequalizer b (f (⊎.inl ⊤.tt*)) eq ∙ SetCoeq.coeq (⊎.inl ⊤.tt*))
                ; (no neq) → refl
                })
              (λ _ → toPathP (SetCoeq.squash _ _ _ _))

            bwd-fwd-help : ∀ x → (notLeft : ¬ (x ≡ SetCoeq.inc (f (⊎.inl ⊤.tt*)))) → fst (bwd (fwd (x , notLeft))) ≡ x
            bwd-fwd-help = CoeqElim
              (λ _ → isSet→ (isSet→isGroupoid SetCoeq.squash _ _))
              (λ b notLeft → toMerge-notLeft notLeft)
              (λ a i → toMerge-notLeft)

            bwd-fwd : ∀ x → bwd (fwd x) ≡ x
            bwd-fwd = λ (x , notLeft) →
              Σ.Σ≡Prop
                (λ x → isProp¬ (x ≡ SetCoeq.inc (f (⊎.inl ⊤.tt*))))
                (bwd-fwd-help x notLeft)

            same-as-new : ⟨ Merge ⟩ ≃ SetCoeq.SetCoequalizer f g
            same-as-new = isoToEquiv (iso fwd bwd fwd-bwd bwd-fwd)
          in FinSet.EquivPresIsFinSet same-as-new (str Merge)
        })
    A B