search

martinescardo / TypeTopology

Logical manifestations of topological concepts, and other things, via the univalent point of view.
GNU General Public License v3.0
220 stars 40 forks source link

The large dcpo of ordinals #282

Closed tomdjong closed 1 month ago

tomdjong commented 1 month ago

Maybe I'm missing something, but presumably the booleans form a small basis, just like for the type of all (small) propositions?

On Mon, 3 Jun 2024, 16:05 Ulrik Buchholtz, @.***> wrote:

@.**** commented on this pull request.

In source/DomainTheory/Examples/Ordinals.lagda https://github.com/martinescardo/TypeTopology/pull/282#discussion_r1624521386 :

  • δ : is-Directed Ordinals-DCPO (directify (family α))
  • δ = directify-is-directed (family α)

  • +Ordinals-DCPO-is-algebraic : is-algebraic-dcpo Ordinals-DCPO +Ordinals-DCPO-is-algebraic = ∣ Ordinals-DCPO-is-algebraic' ∣

  • +\end{code}

  • +Unlike many other examples, such as the dpcos in the Scott model of PCF, or +Scott's D∞, the dpco of ordinals, while algebraic, does not have a small +(compact) basis. If it did, we could take the join of all the basis elements to +obtain a greatest ordinal, which does not exist.

  • +\begin{code}

  • +Ordinals-DCPO-has-no-small-basis : ¬ (has-unspecified-small-basis Ordinals-DCPO)

Nice to have this counterexample formalized. I have yet to find a frame that does not have a small basis.

What about not-not stable propositions (without propositional resizing)?

— Reply to this email directly, view it on GitHub https://github.com/martinescardo/TypeTopology/pull/282#discussion_r1624521386, or unsubscribe https://github.com/notifications/unsubscribe-auth/AKOA4Z7AOLK4ZR4RR6P62P3ZFRZ35AVCNFSM6AAAAABIVFDW3SVHI2DSMVQWIX3LMV43YUDVNRWFEZLROVSXG5CSMV3GSZLXHMZDAOJTHE3TQNRXGE . You are receiving this because you authored the thread.Message ID: @.***>