证明Conat余代数（同伦）终端性的唯一性问题

You've already nailed the existence of the unique homomorphism from any F-coalgebra to ConatCoalgebra using coit. To finish proving homotopy terminality, we need to show any other homomorphism from a coalgebra (C, sc) to ConatCoalgebra is path-equal to the coit-constructed one.

Key Context #

• A coalgebra is homotopy terminal if the space of homomorphisms from any other coalgebra to it is contractible (isContr): meaning there's exactly one homomorphism (up to path equality).
• For coinductive types like Conat, equality is determined by their force fields (via guarded recursion).
• Since Conat is an hSet, function spaces into Conat are also hSets, which simplifies equality proofs for homomorphisms.

Step-by-Step Solution #

Here's how to fill the hole in ConatCoalgebraTerminal:

ConatCoalgebraTerminal : isTerminalCoalgebra ConatCoalgebra
ConatCoalgebraTerminal (C , sc) = (coit.coit sc , λ i s → coit.coitSpec sc s i) , λ y →
  let
    -- Unpack the arbitrary homomorphism we need to equate to our coit-based one
    (f , f-hom) = y

    -- Helper: Build a Conat equality from an equality of their force fields
    -- Guarded by the `i` index in the force field, so it's valid for coinductive types
    conat-path : ∀ {x y : Conat} → force x ≡ force y → x ≡ y
    conat-path p i .force = p i

    -- Prove coit sc s ≡ f s for every s ∈ C (coinductive equality)
    eq : ∀ s → coit sc s ≡ f s
    eq s = conat-path (eq-force s)
      where
        eq-force : ∀ s → force (coit sc s) ≡ force (f s)
        eq-force s with sc s
        -- Case 1: sc s is zero (inl tt)
        ... | inl tt = yesy sc (inl tt) ∙ sym (f-hom s)
        -- Case 2: sc s is successor (inr s'): use coinductive hypothesis (eq s')
        ... | inr s' = yesy sc (inr s') ∙ cong inr (eq s') ∙ sym (f-hom s)

    -- Lift pointwise equality to a function-level path (coit sc ≡ f)
    eq-fun : coit.coit sc ≡ f
    eq-fun = funExt eq

    -- Use hSet properties to show homomorphism proofs are unique (propositional)
    -- First, confirm F Conat is an hSet (since Unit and Conat are hSets)
    isSetFConat : isSet (F Conat)
    isSetFConat = isSetSum isSetUnit isSetConat

    -- The space of functions F C → F Conat is an hSet (codomain is hSet)
    isSetFC→FConat : isSet (F C → F Conat)
    isSetFC→FConat = isSet→isSetFun isSetFConat

    -- Homomorphism proofs are propositional (only one valid path per function)
    hom-prop : isProp (F-map f ∘ sc ≡ force ∘ f)
    hom-prop = isSet→isProp isSetFC→FConat

    -- Transport our coit homomorphism proof along eq-fun to match f-hom
    transport-coitSpec : transport (λ i → F-map (eq-fun i) ∘ sc ≡ force ∘ eq-fun i) (coit.coitSpec sc) ≡ f-hom
    transport-coitSpec = isProp→pathP (λ i → hom-prop) (coit.coitSpec sc) f-hom

    -- Build the final Σ-type path (equates both the function and its homomorphism proof)
    Σ-path : (coit.coit sc , coit.coitSpec sc) ≡ (f , f-hom)
    Σ-path = ΣPathP (eq-fun , transport-coitSpec)
  in
  Σ-path

Breakdown of Critical Parts #

1. conat-path: Since Conat is coinductive, two values are equal if their force fields are equal. This helper constructs such a path directly, and the i index in the force field satisfies Agda's guardedness condition.

2. eq (Pointwise Equality):

   • For each s ∈ C, we prove force (coit sc s) ≡ force (f s):
     • When sc s is zero, both sides reduce to zero; we chain yesy (your existing lemma) with the homomorphism property f-hom.
     • When sc s is succ s', we use the coinductive hypothesis eq s' to show the successor parts are equal, then chain with yesy and f-hom.

3. Function Equality: funExt eq turns pointwise equality into a path between the functions coit sc and f.

4. Propositional Homomorphism Proofs: Since F Conat is an hSet, the space of homomorphism proofs (paths between F-map f ∘ sc and force ∘ f) is a proposition. This means any two valid proofs are equal, so we use isProp→pathP to connect our coitSpec to f-hom.

5. Σ-Type Path: ΣPathP combines the function path and the homomorphism proof path to get the equality of the two Σ-type homomorphisms.

Dependencies #

Make sure you have access to these utilities from Cubical libraries:

• isSetUnit (from Cubical.Data.Unit), isSetSum (from Cubical.Data.Sum)
• Your existing isSetConat proof
• funExt (from Cubical.Foundations.Function)
• ΣPathP and isProp→pathP (from Cubical.Foundations.Path)

内容的提问来源于stack exchange，提问作者Potato44