------------------------------------------------------------------------ -- Code related to the paper "Towards Constructive Hybrid Semantics" -- -- Tim Lukas Diezel and Sergey Goncharov ------------------------------------------------------------------------ {-# OPTIONS --cubical --safe #-} module README where import Sets import Functor import Kleisli import ElgotIteration import PartialOrder import CompletePartialOrder import DecidableOrder import Monoid import MonoidModule import Eliminators-L-wave import Eliminators-L-bar import DurationMonad-L-wave import DurationMonad-L-bar import ChainCompletion import Cantor ------------------------------------------------------------------------ -- Section 2: Preliminaries -- Ordered monoids O-Monoid = Monoid.O-Monoid -- Free objects FreeObject = Functor.FreeObject -- Monads in the form of Kleisli triples Monad = Kleisli.Kleisli -- Elgot iteration ElgotIteration = ElgotIteration.TotalUniConway ------------------------------------------------------------------------ -- Section 3: Hybrid Semantics and Beyond -- Monoid modules MonoidModule = MonoidModule.M-Module ------------------------------------------------------------------------ -- Section 4: Complete Monoid Modules, Categorically -- Complete 𝕄-modules CompleteMonoidModule = MonoidModule.Complete-OM-Module -- Free complete 𝕄-module Free-Complete-𝕄-module = MonoidModule.Initial-Complete-OM-Module-over -- Theorem 7 -- 1. -- Existence of all free objects yields a monad FreeObjects→Monad = Kleisli.FreeObj→Kleisli -- L̃ forms a monad DurationMonad-L̃ = DurationMonad-L-wave.L̃-DurationMonad -- 2. -- Kleisli composition is strict on both sides LeftMonotonicity-L̃ = DurationMonad-L-wave.*-monoˡ RightMonotonicity-L̃ = DurationMonad-L-wave.*-monoʳ LeftContinuity-L̃ = DurationMonad-L-wave.*-contˡ RightContinuity-L̃ = DurationMonad-L-wave.*-contʳ -- 3. -- Iteration operator † on L̃ calculated as a least fixed point Iteration-L̃ = DurationMonad-L-wave.L̃-Iteration -- † satisfies the iteration laws IterationLaws-L̃ = DurationMonad-L-wave.L̃-UniConway ------------------------------------------------------------------------ -- Section 5: Complete Monoid Modules, Classically -- Two equivalent formulations of the axiom of countable choice ACω = Sets.ACω ACω′ = Sets.ACω′ -- Directed chains -- (intensional) DirectedChain = PartialOrder.DirSeq -- (extensional) ‖DirectedChain‖ = PartialOrder.‖DirSeq‖ -- Directed-complete sets -- (intensional) DirectedCompleteSet = CompletePartialOrder.D-CompletePartialOrder -- (extensional) ‖DirectedCompleteSet‖ = CompletePartialOrder.‖D-CompletePartialOrder‖ -- Chain completion ChainCompletion = ChainCompletion.Ã -- Cantor pairing function Cantor = Cantor.π ------------------------------------------------------------------------ -- Section 6: Conservatively Complete Monoid Modules -- Conservatively complete 𝕄-modules Conservatively-Complete-𝕄-Module = MonoidModule.C-Complete-OM-Module -- Theorem 19 -- 1. -- L̅ forms a monad DurationMonad-L̅ = DurationMonad-L-bar.L̅-DurationMonad -- 2. -- Kleisli composition is strict on both sides LeftMonotonicity-L̅ = DurationMonad-L-bar.*-monoˡ RightMonotonicity-L̅ = DurationMonad-L-bar.*-monoʳ LeftContinuity-L̅ = DurationMonad-L-bar.*-contˡ RightContinuity-L̅ = DurationMonad-L-bar.*-contʳ -- 3. -- Iteration operator † on L̅ calculated as a least fixed point Iteration-L̅ = DurationMonad-L-bar.L̅-Iteration -- † satisfies the iteration laws IterationLaws-L̅ = DurationMonad-L-bar.L̅-UniConway ------------------------------------------------------------------------ -- Section 7: Formalization in HoTT/Cubical Agda -- The property of being a (mere) proposition IsProp = Sets.IsProp -- The property of being a set IsSet = Sets.IsSet -- Propositional Truncation ‖_‖ = Sets.‖_‖ -- Increasingness IsIncreasing = PartialOrder.Inc -- Intensional Directedness IsDirected = PartialOrder.Dir -- Extensional Directedness Is‖Directed‖ = PartialOrder.‖Dir‖ -- Proposition 21 -- (a) ⇒ (b) a⇒b = CompletePartialOrder.‖DCPO‖→DCPO -- (b) ⇒ (c) b⇒c = CompletePartialOrder.DCPO→ωCPO -- (b) ⇒ (a) b⇒a = CompletePartialOrder.DCPO→‖DCPO‖ -- (c) ⇒ (a) c⇒a = DecidableOrder.ωCPO→‖DCPO‖ HoTT-Exercise-3-19 = DecidableOrder.restore-ωC -- The HIIT L̃ L̃ = Eliminators-L-wave.Def-L̃.L̃ -- The HIIT L̅ L̅ = Eliminators-L-bar.Def-L̅.L̅ -- Theorem 7.2.2 of the HoTT book HoTT-Theorem-7-2-2 = Sets.A-is-set -- Diagonalization argument for Dir-completeness dseq-dseq→dseq = PartialOrder.dseq-dseq→dseq