- constructive HoTT with propositional resizing and HIITs
- Ω := type of propositions = free DCPPO on 1
- Σ := Rosolini "dominance" (not constructively) / type of semidecidable propositions = conatural numbers quotiented by bisimilarity = (P : Ω) × ∃[ f : ℕ → 2 ] P = (∃[ i : ℕ ] f i = 0)
- Sσ := Sierpiński set = initial σ-frame (higher inductive type [1])
- S∨ := free countably-complete join-semilattice on 1 (higher inductive type [1])
- Sω := free ω-CPPO on 1 (higher inductive-inductive type [2])
- 2 := booleans
- any dominance P induces a mnd-container, hence a monad on sets which I call P-partiality
- Maybe is the 2-partiality monad
- Sσ = Sω = S∨ are dominances [1]
- countable choice → Sσ = Σ → Σ is a dominance [1]
- LEM → Ω = Σ = Sσ = S∨ = Sω = 2
- the free DCPPO adjunction induces the Ω-partiality monad [5] and is not monadic
- the free ω-CPPO adjunction induces the Sω-partiality monad and is not monadic
- the free countably-complete join-semilattice adjunction does not induce the S∨-partiality monad (is it monadic?)
- the free pointed partial order adjunction induces the 2-partiality monad and is not monadic
- the free pointed set adjunction induces the 2-partiality monad and is monadic
- LEM → the free pointed set adjunction is of Kleisli type (classical equivalence between pointed sets and sets-and-partial-functions)
- when does an adjunction F ⊣ U : C → Set induce the UF1-partiality monad? binary joins seem like a no-go. when is UF1 a dominance? when is UF a container monad?
- Quotienting the Delay Monad by Weak Bisimilarity (Chapman et al.)
- Partiality, revisited (Altenkirch et al.)
- Partiality and Container Monads
- https://martinescardo.github.io/TypeTopology/NotionsOfDecidability.SemiDecidable.html
- https://1lab.dev/Order.DCPO.Free.html#free-pointed-dcpos