{-# OPTIONS --without-K #-}
module README.Pointers-to-results-from-the-paper where
import Equality.Propositional as Equality
import Interval
import H-level
import H-level.Truncation.Propositional as Truncation
import Quotient.HIT
import Univalence-axiom
import Delay-monad
import Delay-monad.Alternative
import Delay-monad.Alternative.Equivalence
import Delay-monad.Alternative.Partial-order
import Delay-monad.Alternative.Termination
import Delay-monad.Alternative.Weak-bisimilarity
import Delay-monad.Monad
import Delay-monad.Partial-order
import Delay-monad.Strong-bisimilarity as Strong-bisimilarity
import Delay-monad.Weak-bisimilarity as Weak-bisimilarity
import Lifting
import Partiality-algebra
import Partiality-algebra.Category
import Partiality-algebra.Eliminators
import Partiality-algebra.Fixpoints
import Partiality-algebra.Pi
import Partiality-monad.Coinductive.Alternative
import Partiality-monad.Inductive as Partiality-monad
import Partiality-monad.Inductive.Alternative-order as Alternative-order
import Partiality-monad.Inductive.Eliminators
import Partiality-monad.Inductive.Fixpoints
import Partiality-monad.Inductive.Monad as Monad
import Partiality-monad.Inductive.Monad.Adjunction as Adjunction
import Partiality-monad.Equivalence
import README.Lambda
import Search
Extensionality = Equality.Extensionality
ext = Interval.ext
Delay-ext = Strong-bisimilarity.Extensionality
UIP = Equality.Uniqueness-of-identity-proofs
Is-set = H-level.Is-set
Is-proposition = H-level.Is-proposition
Propositional-extensionality =
Univalence-axiom.Propositional-extensionality
Univalence = Univalence-axiom.Univalence
module Quotient = Quotient.HIT
Countable-choice = Truncation.Axiom-of-countable-choice
Partiality-algebra = Partiality-algebra.Partiality-algebra
Morphism = Partiality-algebra.Morphism
id = Partiality-algebra.id
_∘_ = Partiality-algebra._∘_
category = Partiality-algebra.Category.category
partiality-monad = Partiality-monad.partiality-algebra
_⊥ = Partiality-monad._⊥
Initial = Partiality-algebra.Eliminators.Initial
Induction-principle =
Partiality-algebra.Eliminators.Elimination-principle
universality-to-induction =
Partiality-algebra.Eliminators.∀initiality→∀eliminators
induction-to-universality =
Partiality-algebra.Eliminators.∀eliminators→∀initiality
induction-principle = Partiality-monad.eliminators
Type-is-set = Partiality-algebra.Partiality-algebra-with.Type-is-set
lemma-3 = Partiality-monad.Inductive.Eliminators.⊥-rec-⊥
ω-CPO = Adjunction.ω-CPPO
ω-cpo = Adjunction.ω-cppo
U = Adjunction.Forget
F = Adjunction.Partial
theorem-5 = Adjunction.Partial⊣Forget
corollary-6 = Adjunction.Partiality-monad
μ = Monad.join
module Monad-laws = Monad.Monad-laws
lemma-7-part-1 = Alternative-order.now⊑never≃⊥
lemma-7-part-2 = Alternative-order.now⊑now≃∥≡∥
lemma-7-part-3 = Alternative-order.now⊑⨆≃∥∃now⊑∥
corollary-8-part-1 = Alternative-order.now⊑→⇓
corollary-8-part-2 = Alternative-order.now≡now≃∥≡∥
corollary-8-part-3 = Alternative-order.now≢never
flat-order = Alternative-order.flat-order
Delay = Delay-monad.Delay
_↓D_ = Weak-bisimilarity._⇓_
_∼D_ = Weak-bisimilarity._≈_
_∼D′_ = Weak-bisimilarity._≈′_
∼D⇔∼D′ = Delay-monad.Partial-order.≈⇔≈′
Delay-monad = Delay-monad.Monad.delay-monad
↓D-propositional = Weak-bisimilarity.Terminates-propositional
∼D′-propositional = Weak-bisimilarity.≈′-propositional
∼D-reflexive = Weak-bisimilarity.reflexive
∼D-symmetric = Weak-bisimilarity.symmetric
∼D-transitive = Weak-bisimilarity.transitive
is-mon = Delay-monad.Alternative.Increasing
Seq = Delay-monad.Alternative.Delay
lemma-10 = Delay-monad.Alternative.Equivalence.Delay↔Delay
_↓-Seq_ = Delay-monad.Alternative.Termination._⇓_
↓-Seq⇔∥↓-Seq∥ = Delay-monad.Alternative.Termination.⇓⇔∥⇓∥
_⊑-Seq_ = Delay-monad.Alternative.Partial-order._∥⊑∥_
⊑-Seq-propositional =
Delay-monad.Alternative.Partial-order.∥⊑∥-propositional
_∼-Seq_ = Delay-monad.Alternative.Weak-bisimilarity._≈_
≈-Seq-propositional =
Delay-monad.Alternative.Weak-bisimilarity.≈-propositional
lemma-11 = Partiality-monad.Coinductive.Alternative.⊥↔⊥
w = Partiality-monad.Equivalence.Delay→⊥
w-monotone = Partiality-monad.Equivalence.Delay→⊥-mono
w̃ = Partiality-monad.Equivalence.⊥→⊥
lemma-13 = Partiality-monad.Equivalence.⊥→⊥-injective
lemma-14 = Partiality-monad.Equivalence.Delay→⊥-surjective
w̃-surjective = Partiality-monad.Equivalence.⊥→⊥-surjective
theorem-15-part-1 = Partiality-monad.Equivalence.⊥→⊥-equiv
theorem-15-part-2 = Partiality-monad.Equivalence.⊥≃⊥′
theorem-15-part-3 = Partiality-monad.Equivalence.⊥≃⊥
fix = Partiality-algebra.Fixpoints.fix
fixed-point = Partiality-algebra.Fixpoints.fix-is-fixpoint-combinator
least = Partiality-algebra.Fixpoints.fix-is-least
Π = Partiality-algebra.Pi.Π
module The-search-function = Search.Direct
module Operational-semantics = README.Lambda
module Lifting-construction = Lifting