Martin Escardo, 30 May - 3rd June 2020. Further additions 6th July.

We look at

  * Quasidecidable propositions (generalizing semidecidable propositions).

  * The initial Οƒ-frame.

  * The free Οƒ-sup-lattice on one generator.

Their definitions are given below verbally and in Agda.

We work in a spartan univalent type theory with Ξ , Ξ£, +, Id, 𝟘, πŸ™, β„•,
perhaps W-types, propositional-truncation, univalence, universes. Most
of the time full univalence is not needed - propositional and
functional extenstionality suffice. Sometimes we also consider
propositional resizing, as an explicit assumption each time it is
used.

The above notions don't seem to be definable in our spartan univalent
type theory. Their specifications are as follows:

  * Quasidecidable propositions.

    They are the smallest set of propositions closed under 𝟘,πŸ™, and
    countable existential quantification, or countable joins in the
    frame of propositions.

    They form a dominance.

  * The initial Οƒ-frame.

    A Οƒ-frame has finite meets ⊀ and ∧ and countable joins ⋁, such
    that ∧ distributes over ⋁, with homomorphisms that preserve them.

  * The free Οƒ-sup-lattice on one generator.

    A Οƒ-sup-lattice has an empty join βŠ₯ and countable joins ⋁ with
    homomorphisms that preserve them. It automatically has binary
    joins, which are automatically preserved by homomorphisms.

We have:

 * Quasidecidable propositions exist (the precise definition of
   their existence is given below)  if and only if the free
   Οƒ-sup-lattice on one generator exists.

   The quasidecidable propositions form a dominance.

 * The free Οƒ-sup-lattice on one generator, if it exists, is also the
   initial Οƒ-frame.

   We have that Οƒ-sup-lattice homomorphisms from the free
   Οƒ-sup-lattice on one generator into a Οƒ-frame qua Οƒ-sup-lattice
   automatically preserve finite meets and hence are Οƒ-frame
   homomorphisms.

* Assuming that the free Οƒ-sup-lattice on one generator exists, we
  have that Οƒ-sup-lattices (and hence Οƒ-frames) have joins of families
  indexed by quasidecidable propositions.

\begin{code}

{-# OPTIONS --safe --without-K #-}

open import MLTT.Spartan
open import UF.PropTrunc
open import UF.FunExt
open import UF.Subsingletons
open import UF.SubtypeClassifier renaming (βŠ₯ to βŠ₯Ξ© ; ⊀ to ⊀Ω)
open import UF.SubtypeClassifier-Properties
open import UF.Sets

\end{code}

We assume function extensionality, propositional extensionality and
the existence of propositional truncations, as explicit hypotheses for
this file.

\begin{code}
module NotionsOfDecidability.QuasiDecidable
        (fe  : Fun-Ext)
        (pe  : Prop-Ext)
        (pt  : propositional-truncations-exist)
       where

open import UF.Size

import OrderedTypes.Frame
import OrderedTypes.sigma-frame
import OrderedTypes.sigma-sup-lattice

\end{code}

The following three definitions are parametrized by a universe 𝓣,
which we may wish to be the first universe 𝓀₀ in practice.

We adopt the following notational conventions:

  * 𝓣 is the universe where the quasidecidable truth values live.

    Typically 𝓣 will be 𝓀₀ or 𝓀₁.

  * π“š is the universe where the knowledge they are quasidecidable lives.
    Typically π“š will be 𝓣 or 𝓣 ⁺

Recall that 𝓀, π“₯, 𝓦, 𝓣 range over universes. We add π“š to this list.

\begin{code}

variable π“š : Universe

\end{code}

The notion of existence of quasidecidable propositions, formulated as
a record:

\begin{code}

record quasidecidable-propositions-exist (𝓣 π“š : Universe) : 𝓀ω where
 constructor
  quasidecidable-propositions

 open PropositionalTruncation pt

 field

  is-quasidecidable : 𝓣 Μ‡ β†’ π“š Μ‡

  being-quasidecidable-is-prop : βˆ€ P β†’ is-prop (is-quasidecidable P)

  𝟘-is-quasidecidable : is-quasidecidable 𝟘

  πŸ™-is-quasidecidable : is-quasidecidable πŸ™

  quasidecidable-closed-under-Ο‰-joins
   : (P : β„• β†’ 𝓣 Μ‡ )
   β†’ ((n : β„•) β†’ is-quasidecidable (P n))
   β†’ is-quasidecidable (βˆƒ n κž‰ β„• , P n)

  quasidecidable-induction
   : βˆ€ {𝓀}
     (F : 𝓣 Μ‡ β†’ 𝓀 Μ‡ )
   β†’ ((P : 𝓣 Μ‡ ) β†’ is-prop (F P))
   β†’ F 𝟘
   β†’ F πŸ™
   β†’ ((P : β„• β†’ 𝓣 Μ‡ ) β†’ ((n : β„•) β†’ F (P n)) β†’ F (βˆƒ n κž‰ β„• , P n))
   β†’ (P : 𝓣 Μ‡ ) β†’ is-quasidecidable P β†’ F P

\end{code}

(It follows automatically that quasidecidable types are propositions -
see below.)

We also formulate the existence of the initial Οƒ-frame as a record.

\begin{code}

record initial-Οƒ-frame-exists (𝓣 : Universe) : 𝓀ω where
 constructor
  initial-Οƒ-frame

 open OrderedTypes.sigma-frame fe

 field
  𝓐 : Οƒ-Frame 𝓣
  𝓐-is-initial : {𝓀 : Universe} (𝓑 : Οƒ-Frame 𝓀)
               β†’ βˆƒ! f κž‰ (⟨ 𝓐 ⟩ β†’ ⟨ 𝓑 ⟩), is-Οƒ-frame-hom 𝓐 𝓑 f

\end{code}

And finally the existence of the free Οƒ-sup-lattice on one generator:

\begin{code}

record free-Οƒ-SupLat-on-one-generator-exists (𝓣 π“š : Universe) : 𝓀ω where
 constructor
  free-Οƒ-SupLat-on-one-generator

 open OrderedTypes.sigma-sup-lattice fe

 field
  𝓐 : Οƒ-SupLat 𝓣 π“š
  ⊀ : ⟨ 𝓐 ⟩
  𝓐-free : {π“₯ 𝓦 : Universe} (𝓑 : Οƒ-SupLat π“₯ 𝓦) (t : ⟨ 𝓑 ⟩)
         β†’ βˆƒ! f κž‰ (⟨ 𝓐 ⟩ β†’ ⟨ 𝓑 ⟩) , is-Οƒ-suplat-hom 𝓐 𝓑 f
                                  Γ— (f ⊀ ＝ t)

\end{code}

The main theorems are as follows, where the proofs are given after we
have developed enough material:

\begin{code}

theorem₁ : quasidecidable-propositions-exist 𝓣 π“š
         β†’ free-Οƒ-SupLat-on-one-generator-exists (𝓣 ⁺ βŠ” π“š) 𝓣

theoremβ‚‚ : free-Οƒ-SupLat-on-one-generator-exists 𝓣 𝓀
         β†’ quasidecidable-propositions-exist 𝓣 𝓣

theorem₃ : free-Οƒ-SupLat-on-one-generator-exists 𝓣 π“š
         β†’ initial-Οƒ-frame-exists 𝓣

theoremβ‚„ : Propositional-Resizing
         β†’ quasidecidable-propositions-exist 𝓣 π“š

\end{code}

  * We first work with a hypothetical collection of quasidecidable
    propositions and show that they form the initial Οƒ-frame.

    This is in the submodule hypothetical-quasidecidability.

  * Then we construct it assuming propositional resizing.

    This is in the submodule quasidecidability-construction-from-resizing.

  * Assuming a hypothetical free Οƒ-sup-lattice on one generator, it is
    automatically the initial Οƒ-frame, and from it we can define the
    notion of quasidecidable proposition.

Can we construct them without resizing and without higher-inductive
types other than propositional truncation?

\begin{code}

open PropositionalTruncation pt

open import UF.Base
open import UF.Subsingletons-FunExt
open import UF.Equiv
open import UF.Equiv-FunExt
open import UF.Univalence
open import UF.UA-FunExt
open import UF.EquivalenceExamples
open import UF.Yoneda
open import UF.Embeddings
open import UF.Powerset

open import Dominance.Definition

\end{code}

Before considering quasidecidable propositions, we review
semidecidable ones.

A proposition is semidecidable if it is a countable join of decidable
propositions. See the paper
https://www.cs.bham.ac.uk/~mhe/papers/partial-elements-and-recursion.pdf
by Martin Escardo and Cory Knapp.

NB. Semidecidable propositions are called Rosolini propositions in the above reference.

\begin{code}

is-semidecidable : 𝓀 Μ‡ β†’ 𝓀 Μ‡
is-semidecidable X = βˆƒ Ξ± κž‰ (β„• β†’ 𝟚), X ≃ (βˆƒ n κž‰ β„• , Ξ± n ＝ ₁)

\end{code}

Exercise. X is semidecidable iff it is a countable join of decidable
propositions:

\begin{code}

is-semidecidable' : 𝓀 Μ‡ β†’ 𝓀 ⁺ Μ‡
is-semidecidable' {𝓀} X = βˆƒ A κž‰ (β„• β†’ 𝓀 Μ‡ )
                              , ((n : β„•) β†’ is-decidable (A n))
                              Γ— (X ≃ (βˆƒ n κž‰ β„• , A n))

\end{code}

The following shows that we need to truncate, because the Cantor type
(β„• β†’ 𝟚) is certainly not the type of semidecidable propositions:

\begin{code}

semidecidability-data : 𝓀 Μ‡ β†’ 𝓀 Μ‡
semidecidability-data X = Ξ£ Ξ± κž‰ (β„• β†’ 𝟚), X ≃ (βˆƒ n κž‰ β„• , Ξ± n ＝ ₁)

totality-of-semidecidability-data
 : is-univalent 𝓀₀
 β†’ (Ξ£ X κž‰ 𝓀₀ Μ‡ , semidecidability-data X) ≃ (β„• β†’ 𝟚)
totality-of-semidecidability-data ua =

  (Ξ£ X κž‰ 𝓀₀ Μ‡ , Ξ£ Ξ± κž‰ (β„• β†’ 𝟚), X ≃ (βˆƒ n κž‰ β„• , Ξ± n ＝ ₁)) β‰ƒβŸ¨ i ⟩
  (Ξ£ Ξ± κž‰ (β„• β†’ 𝟚), Ξ£ X κž‰ 𝓀₀ Μ‡ , X ≃ (βˆƒ n κž‰ β„• , Ξ± n ＝ ₁)) β‰ƒβŸ¨ ii ⟩
  (Ξ£ Ξ± κž‰ (β„• β†’ 𝟚), Ξ£ X κž‰ 𝓀₀ Μ‡ , (βˆƒ n κž‰ β„• , Ξ± n ＝ ₁) ≃ X) β‰ƒβŸ¨ iii ⟩
  (β„• β†’ 𝟚) Γ— πŸ™ {𝓀₀}                                      β‰ƒβŸ¨ iv ⟩
  (β„• β†’ 𝟚)                                               β– 
 where
  i   = Ξ£-flip
  ii  = Ξ£-cong (Ξ» Ξ± β†’ Ξ£-cong (Ξ» X β†’ ≃-Sym'' (univalence-gives-funext ua)))
  iii = Ξ£-cong (Ξ» Ξ± β†’ singleton-≃-πŸ™ (univalence-via-singletonsβ†’ ua (βˆƒ n κž‰ β„• , Ξ± n ＝ ₁)))
  iv  = πŸ™-rneutral

𝓒 : 𝓀₁ Μ‡
𝓒 = Ξ£ X κž‰ 𝓀₀ Μ‡ , is-semidecidable X

\end{code}

The type 𝓒 of semidecidable propositions is not a Οƒ-frame unless we
have enough countable choice - see the Escardo-Knapp reference above.

The set of quasidecidable propositions, if it exists, is the smallest
collection of propositions containing 𝟘 and πŸ™ and closed under
countable joins.

Exercise. It exists under propositional resizing assumptions (just
take the intersection of all subsets with 𝟘 and πŸ™ as members and
closed under countable joins). This exercise is solved below in the
submodule quasidecidability-construction-from-resizing.

We now assume that there is a such a smallest collection of types,
called quasidecidable, satisfying the above closure property. The
types in this collection are automatically propositions. The
minimality condition of the collection amounts to an induction
principle.

We recall the above convention:

  * 𝓣 is the universe where the quasidecidable truth values live.

    Typically 𝓣 will be 𝓀₀ or 𝓀₁.

  * π“š is the universe where the knowledge they are quasidecidable lives.

    Typically π“š will be 𝓣 or 𝓣⁺.

\begin{code}

module hypothetical-quasidecidability
        {𝓣 π“š : Universe}
        (qde : quasidecidable-propositions-exist 𝓣 π“š)
       where

\end{code}

As promised, the quasidecidable types are automatically propositions,
with a proof by induction:

\begin{code}

 open quasidecidable-propositions-exist qde

 quasidecidable-types-are-props : βˆ€ P β†’ is-quasidecidable P β†’ is-prop P
 quasidecidable-types-are-props = quasidecidable-induction
                                   is-prop
                                   (Ξ» _ β†’ being-prop-is-prop fe)
                                   𝟘-is-prop
                                   πŸ™-is-prop
                                   (Ξ» P Ο† β†’ βˆƒ-is-prop)

\end{code}

We collect the quasidecidable propositions in the type 𝓠:

\begin{code}

 𝓠 : 𝓣 ⁺ βŠ” π“š Μ‡
 𝓠 = Ξ£ P κž‰ 𝓣 Μ‡ , is-quasidecidable P

 _is-true : 𝓠 β†’ 𝓣 Μ‡
 _is-true (P , i) = P

 being-true-is-quasidecidable : (𝕑 : 𝓠) β†’ is-quasidecidable (𝕑 is-true)
 being-true-is-quasidecidable (P , i) = i

 being-true-is-prop : (𝕑 : 𝓠) β†’ is-prop (𝕑 is-true)
 being-true-is-prop (P , i) = quasidecidable-types-are-props P i

 𝓠→Ω : 𝓠 β†’ Ξ© 𝓣
 𝓠→Ω (P , i) = P , quasidecidable-types-are-props P i

 𝓠→Ω-is-embedding : is-embedding 𝓠→Ω
 𝓠→Ω-is-embedding = NatΞ£-is-embedding is-quasidecidable is-prop ΞΆ ΞΆ-is-embedding
  where
   ΞΆ : (P : 𝓣 Μ‡ ) β†’ is-quasidecidable P β†’ is-prop P
   ΞΆ = quasidecidable-types-are-props

   ΞΆ-is-embedding : (P : 𝓣 Μ‡ ) β†’ is-embedding (ΞΆ P)
   ΞΆ-is-embedding P = maps-of-props-are-embeddings (ΞΆ P)
                       (being-quasidecidable-is-prop P) (being-prop-is-prop fe)

 𝓠-is-set : is-set 𝓠
 𝓠-is-set = subtypes-of-sets-are-sets 𝓠→Ω
             𝓠→Ω-is-embedding
             (Ξ©-is-set fe pe)

 βŠ₯ : 𝓠
 βŠ₯ = 𝟘 , 𝟘-is-quasidecidable

 ⊀ : 𝓠
 ⊀ = πŸ™ , πŸ™-is-quasidecidable

 ⋁ : (β„• β†’ 𝓠) β†’ 𝓠
 ⋁ 𝕑 = (βˆƒ n κž‰ β„• , 𝕑 n is-true) ,
        quasidecidable-closed-under-Ο‰-joins
          (Ξ» n β†’ 𝕑 n is-true)
          (Ξ» n β†’ being-true-is-quasidecidable (𝕑 n))

\end{code}

We formulate and prove induction on 𝓠 in two different, equivalent
ways.

\begin{code}

 𝓠-induction : (G : 𝓠 β†’ 𝓀 Μ‡ )
             β†’ ((𝕑 : 𝓠) β†’ is-prop (G 𝕑))
             β†’ G βŠ₯
             β†’ G ⊀
             β†’ ((𝕑 : β„• β†’ 𝓠) β†’ ((n : β„•) β†’ G (𝕑 n)) β†’ G (⋁ 𝕑))
             β†’ (𝕑 : 𝓠) β†’ G 𝕑

 𝓠-induction {𝓀} G G-is-prop-valued gβ‚€ g₁ gΟ‰ (P , i) = Ξ³
  where
   F :  𝓣 Μ‡ β†’ π“š βŠ” 𝓀 Μ‡
   F P = Ξ£ j κž‰ is-quasidecidable P , G (P , j)

   F-is-prop-valued : βˆ€ P β†’ is-prop (F P)
   F-is-prop-valued P = Ξ£-is-prop
                         (being-quasidecidable-is-prop P)
                         (Ξ» j β†’ G-is-prop-valued (P , j))

   Fβ‚€ : F 𝟘
   Fβ‚€ = 𝟘-is-quasidecidable , gβ‚€

   F₁ : F πŸ™
   F₁ = πŸ™-is-quasidecidable , g₁

   FΟ‰ : (Q : β„• β†’ 𝓣 Μ‡ ) β†’ ((n : β„•) β†’ F (Q n)) β†’ F (βˆƒ n κž‰ β„• , Q n)
   FΟ‰ Q Ο† = quasidecidable-closed-under-Ο‰-joins Q (Ξ» n β†’ pr₁ (Ο† n)) ,
            gΟ‰ (Ξ» n β†’ (Q n , pr₁ (Ο† n))) (Ξ» n β†’ prβ‚‚ (Ο† n))

   Ξ΄ : Ξ£ j κž‰ is-quasidecidable P , G (P , j)
   Ξ΄ = quasidecidable-induction F F-is-prop-valued Fβ‚€ F₁ FΟ‰ P i

   j : is-quasidecidable P
   j = pr₁ Ξ΄

   g : G (P , j)
   g = prβ‚‚ Ξ΄

   r : j ＝ i
   r = being-quasidecidable-is-prop P j i

   Ξ³ : G (P , i)
   Ξ³ = transport (Ξ» - β†’ G (P , -)) r g


 𝓠-induction' : (𝓖 : 𝓠 β†’ Ξ© 𝓀)
              β†’ βŠ₯ ∈ 𝓖
              β†’ ⊀ ∈ 𝓖
              β†’ ((𝕑 : β„• β†’ 𝓠) β†’ ((n : β„•) β†’ 𝕑 n ∈ 𝓖) β†’ ⋁ 𝕑 ∈ 𝓖)
              β†’ (𝕑 : 𝓠) β†’ 𝕑 ∈ 𝓖

 𝓠-induction' {𝓀} 𝓖 = 𝓠-induction (Ξ» 𝕑 β†’ pr₁ (𝓖 𝕑)) (Ξ» 𝕑 β†’ prβ‚‚ (𝓖 𝕑))

\end{code}

The quasidecidable propositions form a dominance, with a proof by
quasidecidable-induction. The main dominance condition generalizes
closure under binary products (that is, conjunctions, or meets):

\begin{code}

 quasidecidable-closed-under-Γ—
  : (P : 𝓣 Μ‡ )
  β†’ is-quasidecidable P
  β†’ (Q : 𝓣 Μ‡ )
  β†’ (P β†’ is-quasidecidable Q)
  β†’ is-quasidecidable (P Γ— Q)
 quasidecidable-closed-under-Γ— =
  quasidecidable-induction F F-is-prop-valued Fβ‚€ F₁ FΟ‰
  where
   F : 𝓣 Μ‡ β†’ 𝓣 ⁺ βŠ” π“š Μ‡
   F P = (Q : 𝓣 Μ‡ ) β†’ (P β†’ is-quasidecidable Q) β†’ is-quasidecidable (P Γ— Q)

   F-is-prop-valued : (P : 𝓣 Μ‡ ) β†’ is-prop (F P)
   F-is-prop-valued P = Ξ β‚‚-is-prop fe
                         (Ξ» Q _ β†’ being-quasidecidable-is-prop (P Γ— Q))

   Fβ‚€ : F 𝟘
   Fβ‚€ Q Ο† = transport is-quasidecidable r 𝟘-is-quasidecidable
    where
     r : 𝟘 ＝ 𝟘 Γ— Q
     r = pe 𝟘-is-prop (Ξ» (z , q) β†’ 𝟘-elim z) unique-from-𝟘 pr₁

   F₁ : F πŸ™
   F₁ Q Ο† = transport is-quasidecidable r (Ο† ⋆)
    where
     i : is-prop Q
     i = quasidecidable-types-are-props Q (Ο† ⋆)

     r : Q ＝ πŸ™ Γ— Q
     r = pe i (Γ—-is-prop πŸ™-is-prop i) (Ξ» q β†’ (⋆ , q)) prβ‚‚

   FΟ‰ :  (P : β„• β†’ 𝓣 Μ‡ ) β†’ ((n : β„•) β†’ F (P n)) β†’ F (βˆƒ n κž‰ β„• , P n)
   Fω P f Q φ = γ
    where
     Ο†' : (n : β„•) β†’ P n β†’ is-quasidecidable Q
     Ο†' n p = Ο† ∣ n , p ∣

     a : (n : β„•) β†’ is-quasidecidable (P n Γ— Q)
     a n = f n Q (Ο†' n)

     b : is-quasidecidable (βˆƒ n κž‰ β„• , P n Γ— Q)
     b = quasidecidable-closed-under-Ο‰-joins (Ξ» n β†’ P n Γ— Q) a

     c : (βˆƒ n κž‰ β„• , P n Γ— Q) β†’ ((βˆƒ n κž‰ β„• , P n) Γ— Q)
     c s = (t , q)
      where
       t : βˆƒ n κž‰ β„• , P n
       t = βˆ₯βˆ₯-rec βˆƒ-is-prop (Ξ» (n , (p , q)) β†’ ∣ n , p ∣) s

       i : is-prop Q
       i = quasidecidable-types-are-props Q (Ο† t)

       q : Q
       q = βˆ₯βˆ₯-rec i (Ξ» (n , (p , q)) β†’ q) s

     d : ((βˆƒ n κž‰ β„• , P n) Γ— Q) β†’ (βˆƒ n κž‰ β„• , P n Γ— Q)
     d (t , q) = βˆ₯βˆ₯-functor (Ξ» (n , p) β†’ n , (p , q)) t

     r : (βˆƒ n κž‰ β„• , P n Γ— Q) ＝ ((βˆƒ n κž‰ β„• , P n) Γ— Q)
     r = pe βˆƒ-is-prop
            (Γ—-prop-criterion ((Ξ» _ β†’ βˆƒ-is-prop) ,
                               (Ξ» e β†’ quasidecidable-types-are-props Q (Ο† e))))
            c d

     Ξ³ : is-quasidecidable ((βˆƒ n κž‰ β„• , P n) Γ— Q)
     Ξ³ = transport is-quasidecidable r b

\end{code}

This condition automatically implies closure under Ξ£, or joins indexed
by quasidecidable propositions:

\begin{code}

 quasidecidable-closed-under-Ξ£
  : (P : 𝓣 Μ‡ )
  β†’ (Q : P β†’ 𝓣 Μ‡ )
  β†’ is-quasidecidable P
  β†’ ((p : P) β†’ is-quasidecidable (Q p))
  β†’ is-quasidecidable (Ξ£ Q)
 quasidecidable-closed-under-Ξ£ =
  D3-and-D5'-give-D5 pe is-quasidecidable
   (quasidecidable-types-are-props)
   (Ξ» P Q' i β†’ quasidecidable-closed-under-Γ— P i Q')

\end{code}

Notice that Ξ£ Q is equivalent to βˆƒ Q as quasidecidable types are
propositions, and propositions are closed under Ξ£:

\begin{code}

 NB : (P : 𝓣 Μ‡ )
    β†’ (Q : P β†’ 𝓣 Μ‡ )
    β†’ is-quasidecidable P
    β†’ ((p : P) β†’ is-quasidecidable (Q p))
    β†’ Ξ£ Q ≃ βˆƒ Q

 NB P Q i j = logically-equivalent-props-are-equivalent
               k
               βˆƒ-is-prop
               (Ξ» (p , q) β†’ ∣ p , q ∣)
               (βˆ₯βˆ₯-rec k id)
  where
   k : is-prop (Ξ£ Q)
   k = quasidecidable-types-are-props
        (Ξ£ Q)
        (quasidecidable-closed-under-Ξ£ P Q i j)

\end{code}

The following summarizes the dominance conditions:

\begin{code}

 quasidecidability-is-dominance : is-dominance is-quasidecidable
 quasidecidability-is-dominance = being-quasidecidable-is-prop ,
                                  quasidecidable-types-are-props ,
                                  πŸ™-is-quasidecidable ,
                                  quasidecidable-closed-under-Ξ£
\end{code}

We now give the quasidecidable propositions the structure of a
Οƒ-sup-lattice. We have already defined βŠ₯, ⊀ and ⋁.

\begin{code}

 _≀_ : 𝓠 β†’ 𝓠 β†’ 𝓣 Μ‡
 𝕑 ≀ 𝕒 = 𝕑 is-true β†’ 𝕒 is-true

 ≀-is-prop-valued : (𝕑 𝕒 : 𝓠) β†’ is-prop (𝕑 ≀ 𝕒)
 ≀-is-prop-valued 𝕑 𝕒 = Ξ -is-prop fe (Ξ» _ β†’ being-true-is-prop 𝕒)

 ≀-refl : (𝕑 : 𝓠) β†’ 𝕑 ≀ 𝕑
 ≀-refl 𝕑 = id

 ≀-trans : (𝕑 𝕒 𝕣 : 𝓠) β†’ 𝕑 ≀ 𝕒 β†’ 𝕒 ≀ 𝕣 β†’ 𝕑 ≀ 𝕣
 ≀-trans 𝕑 𝕒 𝕣 l m = m ∘ l

 ≀-antisym : (𝕑 𝕒 : 𝓠) β†’ 𝕑 ≀ 𝕒 β†’ 𝕒 ≀ 𝕑 β†’ 𝕑 ＝ 𝕒
 ≀-antisym 𝕑 𝕒 l m = to-subtype-＝
                      being-quasidecidable-is-prop
                      (pe (being-true-is-prop 𝕑) (being-true-is-prop 𝕒) l m)

 βŠ₯-is-minimum : (𝕑 : 𝓠) β†’ βŠ₯ ≀ 𝕑
 βŠ₯-is-minimum 𝕑 = unique-from-𝟘

 ⊀-is-maximum : (𝕑 : 𝓠) β†’ 𝕑 ≀ ⊀
 ⊀-is-maximum 𝕑 = unique-to-πŸ™

 ⋁-is-ub : (𝕑 : β„• β†’ 𝓠) β†’ (n : β„•) β†’ 𝕑 n ≀ ⋁ 𝕑
 ⋁-is-ub 𝕑 n = (Ξ» p β†’ ∣ n , p ∣)

 ⋁-is-lb-of-ubs : (𝕑 : β„• β†’ 𝓠) β†’ (𝕦 : 𝓠) β†’ ((n : β„•) β†’ 𝕑 n ≀ 𝕦) β†’ ⋁ 𝕑 ≀ 𝕦
 ⋁-is-lb-of-ubs 𝕑 (U , i) Ο† = Ξ³
  where
   Ξ΄ : (Ξ£ n κž‰ β„• , 𝕑 n is-true) β†’ U
   Ξ΄ (n , p) = Ο† n p

   Ξ³ : (βˆƒ n κž‰ β„• , 𝕑 n is-true) β†’ U
   Ξ³ = βˆ₯βˆ₯-rec (quasidecidable-types-are-props U i) Ξ΄

\end{code}

Putting these axioms together we get the Οƒ-sup-lattice of
quasidecidable propositions:

\begin{code}

 open import OrderedTypes.sigma-sup-lattice fe

 QD : Οƒ-SupLat (𝓣 ⁺ βŠ” π“š) 𝓣
 QD = 𝓠 ,
     (βŠ₯ , ⋁) ,
     _≀_ ,
     ≀-is-prop-valued ,
     ≀-refl ,
     ≀-trans ,
     ≀-antisym ,
     βŠ₯-is-minimum ,
     ⋁-is-ub ,
     ⋁-is-lb-of-ubs

\end{code}

We now show that QD is the free Οƒ-sup-lattice on one generator. For
this purpose, we assume that we are give a Οƒ-sup-lattice 𝓐 with a
distinguished element t.

\begin{code}

 module _ {𝓀 π“₯ : Universe}
          (𝓐 : Οƒ-SupLat 𝓀 π“₯)
          (t : ⟨ 𝓐 ⟩)
        where

\end{code}

We introduce some abbreviations, private to this anonymous module, for
notational convenience:

\begin{code}

  private

    A = ⟨ 𝓐 ⟩
    βŠ₯' = βŠ₯⟨ 𝓐 ⟩
    ⋁' = β‹βŸ¨ 𝓐 ⟩
    _≀'_ : A β†’ A β†’ π“₯ Μ‡
    a ≀' b = a β‰€βŸ¨ 𝓐 ⟩ b

\end{code}

And then again by 𝓠-induction, there is at most one homomorphism from
𝓠 to 𝓐:

\begin{code}

  at-most-one-hom : (g h : 𝓠 β†’ A)
                  β†’ is-Οƒ-suplat-hom QD 𝓐 g
                  β†’ is-Οƒ-suplat-hom QD 𝓐 h
                  β†’ g ⊀ ＝ t
                  β†’ h ⊀ ＝ t
                  β†’ g ＝ h
  at-most-one-hom g h (gβŠ₯ , g⋁) (hβŠ₯ , h⋁) g⊀ h⊀ = dfunext fe r
   where
    iβ‚€ = g βŠ₯ ＝⟨ gβŠ₯ ⟩
         βŠ₯'  ＝⟨ hβŠ₯ ⁻¹ ⟩
         h βŠ₯ ∎

    i₁ = g ⊀ ＝⟨ g⊀ ⟩
         t   ＝⟨ h⊀ ⁻¹ ⟩
         h ⊀ ∎

    iΟ‰ : (𝕑 : β„• β†’ 𝓠) β†’ ((n : β„•) β†’ g (𝕑 n) ＝ h (𝕑 n)) β†’ g (⋁ 𝕑) ＝ h (⋁ 𝕑)
    iΟ‰ 𝕑 Ο† = g (⋁ 𝕑)          ＝⟨ g⋁ 𝕑 ⟩
             ⋁' (n ↦ g (𝕑 n)) ＝⟨ ap ⋁' (dfunext fe Ο†) ⟩
             ⋁' (n ↦ h (𝕑 n)) ＝⟨ (h⋁ 𝕑)⁻¹ ⟩
             h (⋁ 𝕑)          ∎

    r : g ∼ h
    r = 𝓠-induction (Ξ» 𝕑 β†’ g 𝕑 ＝ h 𝕑) (Ξ» 𝕑 β†’ ⟨ 𝓐 ⟩-is-set {g 𝕑} {h 𝕑}) iβ‚€ i₁ iΟ‰

\end{code}

The condition in the conclusion of the following lemma says that the
element a : A is the least upper bound of the (weakly) constant family
Ξ» (p : P) β†’ ⊀'.  Because least upper bounds are unique when they
exist, the type in the conclusion of the lemma is a proposition. This
is crucial because the induction principle can be applied to
prop-valued predicates only.

\begin{code}

  freeness-lemma : (P : 𝓣 Μ‡ )
                 β†’ is-quasidecidable P
                 β†’ Ξ£ a κž‰ A , (P β†’ t ≀' a) Γ— ((u : A) β†’ (P β†’ t ≀' u) β†’ a ≀' u)

  freeness-lemma = quasidecidable-induction F F-is-prop-valued Fβ‚€ F₁ FΟ‰
   where
    F : 𝓣 Μ‡ β†’ 𝓣 βŠ” 𝓀 βŠ” π“₯ Μ‡
    F P = Ξ£ a κž‰ A , (P β†’ t ≀' a) Γ— ((u : A) β†’ (P β†’ t ≀' u) β†’ a ≀' u)

    F-is-prop-valued : (P : 𝓣 Μ‡ ) β†’ is-prop (F P)
    F-is-prop-valued P (a , Ξ± , Ξ²) (a' , Ξ±' , Ξ²') = Ξ³
     where
      j : (a : A) β†’ is-prop ((P β†’ t ≀' a) Γ— ((u : A) β†’ (P β†’ t ≀' u) β†’ a ≀' u))
      j a = Γ—-is-prop
             (Ξ -is-prop fe (Ξ» _ β†’ ⟨ 𝓐 ⟩-order-is-prop-valued t a))
             (Ξ β‚‚-is-prop fe (Ξ» u _ β†’ ⟨ 𝓐 ⟩-order-is-prop-valued a u))

      r : a ＝ a'
      r = ⟨ 𝓐 ⟩-antisym a a' (Ξ²  a' Ξ±') (Ξ²' a Ξ±)

      γ : (a , α , β) ＝ (a' , α' , β')
      γ = to-subtype-＝ j r

    Fβ‚€ : F 𝟘
    Fβ‚€ = βŠ₯' , unique-from-𝟘 , (Ξ» u ψ β†’ ⟨ 𝓐 ⟩-βŠ₯-is-minimum u)

    F₁ : F πŸ™
    F₁ = t , (Ξ» _ β†’ ⟨ 𝓐 ⟩-refl t) , (Ξ» u ψ β†’ ψ ⋆)

    FΟ‰ :  (P : β„• β†’ 𝓣 Μ‡ ) β†’ ((n : β„•) β†’ F (P n)) β†’ F (βˆƒ n κž‰ β„• , P n)
    FΟ‰ P Ο† = a∞ , α∞ , β∞
     where
      a : β„• β†’ A
      a n = pr₁ (Ο† n)

      Ξ± : (n : β„•) β†’ P n β†’ t ≀' a n
      Ξ± n = pr₁ (prβ‚‚ (Ο† n))

      Ξ² : (n : β„•) (u : A) β†’ (P n β†’ t ≀' u) β†’ a n ≀' u
      Ξ² n = prβ‚‚ (prβ‚‚ (Ο† n))

      a∞ : A
      a∞ = ⋁' a

      α∞ : (βˆƒ n κž‰ β„• , P n) β†’ t ≀' a∞
      α∞ = βˆ₯βˆ₯-rec (⟨ 𝓐 ⟩-order-is-prop-valued t a∞)  α∞'
       where
        α∞' : (Ξ£ n κž‰ β„• , P n) β†’ t ≀' a∞
        α∞' (n , p) = ⟨ 𝓐 ⟩-trans t (a n) a∞ (Ξ± n p) (⟨ 𝓐 ⟩-⋁-is-ub a n)

      β∞ : (u : A) β†’ ((βˆƒ n κž‰ β„• , P n) β†’ t ≀' u) β†’ a∞ ≀' u
      β∞ u ψ = ⟨ 𝓐 ⟩-⋁-is-lb-of-ubs a u l
       where
        l : (n : β„•) β†’ a n ≀' u
        l n = Ξ² n u (Ξ» p β†’ ψ ∣ n , p ∣)

\end{code}

We now have enough constructions and lemmas to show that the type of
quasidecidable propositions is the free Οƒ-sup-lattice on one
generator. It remains to show that the function 𝓠 β†’ A induced by the
initiality lemma is a Οƒ-sup-lattice homomorphism.

\begin{code}

  QD-is-free-Οƒ-SupLat : βˆƒ! f κž‰ (⟨ QD ⟩ β†’ ⟨ 𝓐 ⟩) , is-Οƒ-suplat-hom QD 𝓐 f
                                                Γ— (f ⊀ ＝ t)
  QD-is-free-Οƒ-SupLat = Ξ³
   where
    f : 𝓠 β†’ A
    f (P , i) = pr₁ (freeness-lemma P i)

    Ξ± : (𝕑 : 𝓠) β†’ 𝕑 is-true β†’ t ≀' f 𝕑
    Ξ± (P , i) = pr₁ (prβ‚‚ (freeness-lemma P i))

    Ξ² : (𝕑 : 𝓠) β†’ ((u : A) β†’ (𝕑 is-true β†’ t ≀' u) β†’ f 𝕑 ≀' u)
    Ξ² (P , i) = prβ‚‚ (prβ‚‚ (freeness-lemma P i))

\end{code}

The conditions Ξ± and Ξ² on f are crucial to prove that f is indeed a
homomorphism, and are all we need for that purpose.

\begin{code}

    f⊀ : f ⊀ ＝ t
    f⊀ = ⟨ 𝓐 ⟩-antisym (f ⊀) t (Ξ² ⊀ t (Ξ» _ β†’ ⟨ 𝓐 ⟩-refl t)) (Ξ± ⊀ ⋆)

    fβŠ₯ : f βŠ₯ ＝ βŠ₯'
    fβŠ₯ = ⟨ 𝓐 ⟩-antisym (f βŠ₯) βŠ₯' (Ξ² βŠ₯ βŠ₯' unique-from-𝟘) (⟨ 𝓐 ⟩-βŠ₯-is-minimum (f βŠ₯))

    f-is-monotone : (𝕑 𝕒 : 𝓠) β†’ 𝕑 ≀ 𝕒 β†’ f 𝕑 ≀' f 𝕒
    f-is-monotone 𝕑 𝕒 l = Ξ² 𝕑 (f 𝕒) (Ξ» p β†’ Ξ± 𝕒 (l p))

    f⋁ : (𝕑 : β„• β†’ 𝓠) β†’ f (⋁ 𝕑) ＝ ⋁' (n ↦ f (𝕑 n))
    f⋁ 𝕑 = ⟨ 𝓐 ⟩-antisym (f (⋁ 𝕑)) (⋁' (n ↦ f (𝕑 n))) v w
      where
       Ο†' : (Ξ£ n κž‰ β„• , 𝕑 n is-true) β†’ t ≀' ⋁' (n ↦ f (𝕑 n))
       Ο†' (n , p) = ⟨ 𝓐 ⟩-trans t (f (𝕑 n)) (⋁' (n ↦ f (𝕑 n))) r s
         where
          r : t ≀' f (𝕑 n)
          r = Ξ± (𝕑 n) p

          s : f (𝕑 n) ≀' ⋁' (n ↦ f (𝕑 n))
          s = ⟨ 𝓐 ⟩-⋁-is-ub (n ↦ f (𝕑 n)) n

       Ο† : (βˆƒ n κž‰ β„• , 𝕑 n is-true) β†’ t ≀' ⋁' (n ↦ f (𝕑 n))
       Ο† = βˆ₯βˆ₯-rec (⟨ 𝓐 ⟩-order-is-prop-valued _ _) Ο†'

       v : f (⋁ 𝕑) ≀' ⋁' (n ↦ f (𝕑 n))
       v = Ξ² (⋁ 𝕑) (⋁' (n ↦ f (𝕑 n))) Ο†

       l : (n : β„•) β†’ 𝕑 n ≀ ⋁ 𝕑
       l = ⋁-is-ub 𝕑

       m : (n : β„•) β†’ f (𝕑 n) ≀' f (⋁ 𝕑)
       m n = f-is-monotone (𝕑 n) (⋁ 𝕑) (l n)

       w : ⋁' (n ↦ f (𝕑 n)) ≀' f (⋁ 𝕑)
       w = ⟨ 𝓐 ⟩-⋁-is-lb-of-ubs (n ↦ f (𝕑 n)) (f (⋁ 𝕑)) m

\end{code}

And then we are done:

\begin{code}

    f-is-hom : is-Οƒ-suplat-hom QD 𝓐 f
    f-is-hom = fβŠ₯ , f⋁

    Ξ³ : βˆƒ! f κž‰ (⟨ QD ⟩ β†’ A) , is-Οƒ-suplat-hom QD 𝓐 f
                            Γ— (f ⊀ ＝ t)
    γ = (f , f-is-hom , f⊀) ,
        (Ξ» (g , g-is-hom , g⊀) β†’ to-subtype-＝
                                  (Ξ» f β†’ Γ—-is-prop
                                          (being-Οƒ-suplat-hom-is-prop QD 𝓐 f)
                                          ⟨ 𝓐 ⟩-is-set)
                                  (at-most-one-hom f g f-is-hom g-is-hom f⊀ g⊀))
\end{code}

This concludes the module hypothetical-quasidecidability.

We discussed above the specification of the notion of quasidecidable
proposition. But can we define or construct it? Yes if, for example,
propositional resizing is available:

\begin{code}


module quasidecidability-construction-from-resizing
        (𝓣 π“š : Universe)
        (ρ : Propositional-Resizing)
       where

 open import UF.Powerset-Resizing fe ρ

\end{code}

This assumption says that any proposition in the universe 𝓀 is
equivalent to some proposition in the universe π“₯, for any two
universes 𝓀 and π“₯.

The crucial fact exploited here is that intersections of collections
of subcollections 𝓐 : π“Ÿ (π“Ÿ X) exist under propositional resizing.

To define the type of quasi-decidable propositions, we take the
intersection of the collections of types satisfying the following
closure condition:

\begin{code}

 QD-closed-types : (𝓀 Μ‡ β†’ Ξ© π“₯) β†’ Ξ© (𝓀 ⁺ βŠ” π“₯)
 QD-closed-types {𝓀} {π“₯} A = closure-condition , i
  where
   closure-condition : 𝓀 ⁺ βŠ” π“₯ Μ‡
   closure-condition = (𝟘 ∈ A)
                     Γ— (πŸ™ ∈ A)
                     Γ— ((P : β„• β†’ 𝓀 Μ‡ ) β†’ ((n : β„•) β†’ P n ∈ A) β†’ (βˆƒ n κž‰ β„• , P n) ∈ A)

   i : is-prop closure-condition
   i = ×₃-is-prop (∈-is-prop A 𝟘)
                  (∈-is-prop A πŸ™)
                  (Ξ β‚‚-is-prop fe (Ξ» P _ β†’ ∈-is-prop A (βˆƒ n κž‰ β„• , P n)))

 is-quasidecidable : 𝓣 Μ‡ β†’ π“š Μ‡
 is-quasidecidable P = P ∈ β‹‚ QD-closed-types

 being-quasidecidable-is-prop : βˆ€ P β†’ is-prop (is-quasidecidable P)
 being-quasidecidable-is-prop = ∈-is-prop (β‹‚ QD-closed-types)

 𝟘-is-quasidecidable : is-quasidecidable 𝟘
 𝟘-is-quasidecidable = to-β‹‚ QD-closed-types 𝟘 (Ξ» A (cβ‚€ , c₁ , cΟ‰) β†’ cβ‚€)

 πŸ™-is-quasidecidable : is-quasidecidable πŸ™
 πŸ™-is-quasidecidable = to-β‹‚ QD-closed-types πŸ™ (Ξ» A (cβ‚€ , c₁ , cΟ‰) β†’ c₁)

 quasidecidable-closed-under-Ο‰-joins : (P : β„• β†’ 𝓣 Μ‡ )
                                     β†’ ((n : β„•) β†’ is-quasidecidable (P n))
                                     β†’ is-quasidecidable (βˆƒ n κž‰ β„• , P n)

 quasidecidable-closed-under-Ο‰-joins P Ο† = to-β‹‚ QD-closed-types (βˆƒ P) vi
  where
   i : (n : β„•) β†’ P n ∈ β‹‚ QD-closed-types
   i = Ο†

   ii : (n : β„•) (A : 𝓣 Μ‡ β†’ Ξ© π“š) β†’ A ∈ QD-closed-types β†’ P n ∈ A
   ii n = from-β‹‚ QD-closed-types (P n) (i n)

   iii : (A : 𝓣 Μ‡ β†’ Ξ© π“š) β†’ A ∈ QD-closed-types β†’ βˆƒ P ∈ A
   iii A (c₁ , cβ‚‚ , cΟ‰) = cΟ‰ P (Ξ» n β†’ ii n A (c₁ , cβ‚‚ , cΟ‰))

   iv : βˆƒ P ∈ β‹‚ QD-closed-types
   iv = to-β‹‚ QD-closed-types (βˆƒ P) iii

   vi : (A : 𝓣 Μ‡ β†’ Ξ© π“š) β†’ A ∈ QD-closed-types β†’ βˆƒ P ∈ A
   vi = from-β‹‚ QD-closed-types (βˆƒ P) iv

\end{code}

The full induction principle requires a further application of
resizing. We first prove a particular case and then reduce the general
case to this particular case.

\begin{code}

 quasidecidable-inductionβ‚€ :
     (F : 𝓣 Μ‡ β†’ π“š Μ‡ )
   β†’ ((P : 𝓣 Μ‡ ) β†’ is-prop (F P))
   β†’ F 𝟘
   β†’ F πŸ™
   β†’ ((P : β„• β†’ 𝓣 Μ‡ ) β†’ ((n : β„•) β†’ F (P n)) β†’ F (βˆƒ n κž‰ β„• , P n))
   β†’ (P : 𝓣 Μ‡ ) β†’  is-quasidecidable P β†’ F P

 quasidecidable-inductionβ‚€ F F-is-prop-valued Fβ‚€ F₁ FΟ‰ P P-is-quasidecidable = Ξ³
  where
   A : (P : 𝓣 Μ‡ ) β†’ Ξ© π“š
   A P = F P , F-is-prop-valued P

   A-is-QD-closed : A ∈ QD-closed-types
   A-is-QD-closed = Fβ‚€ , F₁ , FΟ‰

   pqd : P ∈ β‹‚ QD-closed-types
   pqd = P-is-quasidecidable

   δ : P ∈ A
   Ξ΄ = from-β‹‚ QD-closed-types P pqd A A-is-QD-closed

   Ξ³ : F P
   Ξ³ = Ξ΄

\end{code}

To get the full induction principle we apply the above particular case
with back and forth resizing coercions. The point is that now F has
values in any universe 𝓀 rather than the universe π“š as above.

\begin{code}

 quasidecidable-induction
  : (F : 𝓣 Μ‡ β†’ 𝓀 Μ‡ )
  β†’ ((P : 𝓣 Μ‡ ) β†’ is-prop (F P))
  β†’ F 𝟘
  β†’ F πŸ™
  β†’ ((P : β„• β†’ 𝓣 Μ‡ ) β†’ ((n : β„•) β†’ F (P n)) β†’ F (βˆƒ n κž‰ β„• , P n))
  β†’ (P : 𝓣 Μ‡ ) β†’ is-quasidecidable P β†’ F P
 quasidecidable-induction {𝓀} F F-is-prop-valued Fβ‚€ F₁ FΟ‰ P P-is-quasidecidable =
  Ξ³
  where
   i = F-is-prop-valued

   F' : 𝓣 Μ‡ β†’ π“š Μ‡
   F' P = resize ρ (F P) (i P)

   i' : (P : 𝓣 Μ‡ ) β†’ is-prop (F' P)
   i' P = resize-is-prop ρ (F P) (i P)

   Ξ΄ : F' P
   Ξ΄ = quasidecidable-inductionβ‚€
        F'
        i'
        (to-resize ρ (F 𝟘) (i 𝟘) Fβ‚€)
        (to-resize ρ (F πŸ™) (i πŸ™) F₁)
        (Ξ» P Q β†’ to-resize ρ
                  (F (βˆƒ P))
                  (i (βˆƒ P))
                  (FΟ‰ P (Ξ» n β†’ from-resize ρ
                                (F (P n))
                                (i (P n))
                                (Q n))))
        P
        P-is-quasidecidable

   Ξ³ : F P
   γ = from-resize ρ (F P) (i P) δ

\end{code}

Hence the free Οƒ-sup-lattice on one generator exists under
propositional resizing: we simply plug the construction of the
quasidecidable propositions to the above hypothetical development.

\begin{code}

 open OrderedTypes.sigma-sup-lattice fe

 free-Οƒ-suplat-on-one-generator-exists
  : Ξ£ 𝓐 κž‰ Οƒ-SupLat (𝓣 ⁺ βŠ” π“š) 𝓣
  , Ξ£ t κž‰ ⟨ 𝓐 ⟩
  , ((𝓑 : Οƒ-SupLat 𝓀 π“₯) (u : ⟨ 𝓑 ⟩)
        β†’ βˆƒ! f κž‰ (⟨ 𝓐 ⟩ β†’ ⟨ 𝓑 ⟩) , is-Οƒ-suplat-hom 𝓐 𝓑 f
                                  Γ— (f t ＝ u))
 free-Οƒ-suplat-on-one-generator-exists {𝓀} {π“₯} = QD , ⊀ , QD-is-free-Οƒ-SupLat
  where
   open hypothetical-quasidecidability
          (quasidecidable-propositions
             is-quasidecidable
             being-quasidecidable-is-prop
             𝟘-is-quasidecidable
             πŸ™-is-quasidecidable
             quasidecidable-closed-under-Ο‰-joins
             quasidecidable-induction)
\end{code}

This concludes the module quasidecidability-construction-from-resizing.

The initial Οƒ-frame can also be constructed as a higher-inductive
type, as is well known.

The initial Οƒ-sup-lattice is automatically the initial Οƒ-frame. This
is shown below.

TODO. Write in Agda some of the proofs of the above reference with
Cory Knapp, particularly regarding choice. E.g. the semidecidable
properties form a dominance if and only if a certain particular case
of countable choice holds.

TODO. This certain particular case of countable choice holds if and
only if the quasidecidable propositions are semidecidable. This is not
in the paper, but the methods of proof of the paper should apply more
or less directly.

To think about. Can we construct the collection of quasidecidable
propositions without resizing and without higher-inductive types other
than propositional truncation?

We now explore the consequences of the hypothetical existence of an
free Οƒ-sup-lattice on one generator ⊀.

\begin{code}

module hypothetical-free-Οƒ-SupLat-on-one-generator where

 open import OrderedTypes.sigma-sup-lattice fe

 module assumption
        {𝓣 π“š : Universe}
        (𝓐 : Οƒ-SupLat 𝓣 π“š)
        (⊀ : ⟨ 𝓐 ⟩)
        (𝓐-free : {π“₯ 𝓦 : Universe} (𝓑 : Οƒ-SupLat π“₯ 𝓦) (t : ⟨ 𝓑 ⟩)
                β†’ βˆƒ! f κž‰ (⟨ 𝓐 ⟩ β†’ ⟨ 𝓑 ⟩) , is-Οƒ-suplat-hom 𝓐 𝓑 f
                                         Γ— (f ⊀ ＝ t))
        where

\end{code}

We first introduce some abbreviations:

\begin{code}

  private
   A   = ⟨ 𝓐 ⟩
   βŠ₯   = βŠ₯⟨ 𝓐 ⟩
   ⋁  = β‹βŸ¨ 𝓐 ⟩

  _≀_ : A β†’ A β†’ π“š Μ‡
  a ≀ b = a β‰€βŸ¨ 𝓐 ⟩ b

  Οƒ-rec : (𝓑 : Οƒ-SupLat π“₯ 𝓦) (t : ⟨ 𝓑 ⟩) β†’ ⟨ 𝓐 ⟩ β†’ ⟨ 𝓑 ⟩
  Οƒ-rec 𝓑 t = pr₁ (center (𝓐-free 𝓑 t))

  Οƒ-rec-is-hom : (𝓑 : Οƒ-SupLat π“₯ 𝓦) (t : ⟨ 𝓑 ⟩)
               β†’ is-Οƒ-suplat-hom 𝓐 𝓑 (Οƒ-rec 𝓑 t)
  Οƒ-rec-is-hom 𝓑 t = pr₁ (prβ‚‚ (center (𝓐-free 𝓑 t)))

  Οƒ-rec-βŠ₯ : (𝓑 : Οƒ-SupLat π“₯ 𝓦) (t : ⟨ 𝓑 ⟩)
          β†’ Οƒ-rec 𝓑 t βŠ₯ ＝ βŠ₯⟨ 𝓑 ⟩
  Οƒ-rec-βŠ₯ 𝓑 t = Οƒ-suplat-hom-βŠ₯ 𝓐 𝓑 (Οƒ-rec 𝓑 t) (Οƒ-rec-is-hom 𝓑 t)

  Οƒ-rec-⋁ : (𝓑 : Οƒ-SupLat π“₯ 𝓦) (t : ⟨ 𝓑 ⟩) (a : β„• β†’ A)
          β†’ Οƒ-rec 𝓑 t (⋁ a) ＝ β‹βŸ¨ 𝓑 ⟩ (n ↦ Οƒ-rec 𝓑 t (a n))
  Οƒ-rec-⋁ 𝓑 t = Οƒ-suplat-hom-⋁ 𝓐 𝓑 (Οƒ-rec 𝓑 t) (Οƒ-rec-is-hom 𝓑 t)

  Οƒ-rec-⊀ : (𝓑 : Οƒ-SupLat π“₯ 𝓦) (t : ⟨ 𝓑 ⟩)
          β†’ Οƒ-rec 𝓑 t ⊀ ＝ t
  Οƒ-rec-⊀ 𝓑 t = prβ‚‚ (prβ‚‚ (center (𝓐-free 𝓑 t)))

  Οƒ-rec-is-unique : (𝓑 : Οƒ-SupLat π“₯ 𝓦) (t : ⟨ 𝓑 ⟩)
                    (f : A β†’ ⟨ 𝓑 ⟩)
                  β†’ is-Οƒ-suplat-hom 𝓐 𝓑 f
                  β†’ f ⊀ ＝ t
                  β†’ Οƒ-rec 𝓑 t ＝ f
  Οƒ-rec-is-unique 𝓑 t f i p = ap pr₁ (centrality (𝓐-free 𝓑 t) (f , i , p))

  at-most-one-hom : (𝓑 : Οƒ-SupLat π“₯ 𝓦) (t : ⟨ 𝓑 ⟩)
                    (f g : A β†’ ⟨ 𝓑 ⟩)
                  β†’ is-Οƒ-suplat-hom 𝓐 𝓑 f
                  β†’ is-Οƒ-suplat-hom 𝓐 𝓑 g
                  β†’ f ⊀ ＝ t
                  β†’ g ⊀ ＝ t
                  β†’ f ＝ g
  at-most-one-hom 𝓑 t f g i j p q = ap pr₁
                                       (singletons-are-props
                                         (𝓐-free 𝓑 t)
                                         (f , i , p)
                                         (g , j , q))
\end{code}

We now establish the induction principle for the free Οƒ-sup-lattice on
one generator by constructing a Οƒ-sup-lattice from the property we
want to prove.

\begin{code}

  Οƒ-induction : (P : A β†’ π“₯ Μ‡ )
              β†’ ((a : A) β†’ is-prop (P a))
              β†’ P ⊀
              β†’ P βŠ₯
              β†’ ((a : (β„• β†’ A)) β†’ ((n : β„•) β†’ P (a n)) β†’ P (⋁ a))
              β†’ (a : A) β†’ P a
  Οƒ-induction {π“₯} P P-is-prop-valued ⊀-closure βŠ₯-closure ⋁-closure = Ξ³
   where
    X = Ξ£ a κž‰ A , P a

    ⊀' βŠ₯' : X
    ⊀' = (⊀ , ⊀-closure)
    βŠ₯' = (βŠ₯ , βŠ₯-closure)

    ⋁' : (β„• β†’ X) β†’ X
    ⋁' x = (⋁ (pr₁ ∘ x) , ⋁-closure (pr₁ ∘ x) (prβ‚‚ ∘ x))

    _≀'_ : X β†’ X β†’ π“š Μ‡
    (a , _) ≀' (b , _) = a ≀ b

    𝓑 : Οƒ-SupLat (𝓣 βŠ” π“₯) π“š
    𝓑 = X , (βŠ₯' , ⋁') ,
         _≀'_ ,
         (Ξ» (a , _) (b , _) β†’ ⟨ 𝓐 ⟩-order-is-prop-valued a b) ,
         (Ξ» (a , _) β†’ ⟨ 𝓐 ⟩-refl a) ,
         (Ξ» (a , _) (b , _) (c , _) β†’ ⟨ 𝓐 ⟩-trans a b c) ,
         (Ξ» (a , _) (b , _) l m β†’ to-subtype-＝
                                   P-is-prop-valued
                                   (⟨ 𝓐 ⟩-antisym a b l m)) ,
         (Ξ» (a , _) β†’ ⟨ 𝓐 ⟩-βŠ₯-is-minimum a) ,
         (Ξ» x n β†’ ⟨ 𝓐 ⟩-⋁-is-ub (pr₁ ∘ x) n) ,
         (Ξ» x (u , _) Ο† β†’ ⟨ 𝓐 ⟩-⋁-is-lb-of-ubs (pr₁ ∘ x) u Ο†)

    g : X β†’ A
    g = pr₁

    g-is-hom : is-Οƒ-suplat-hom 𝓑 𝓐 g
    g-is-hom = refl , (Ξ» 𝕒 β†’ refl)

    h : A β†’ A
    h = g ∘ Οƒ-rec 𝓑 ⊀'

    h⊀ : h ⊀ ＝ ⊀
    h⊀ = ap g (Οƒ-rec-⊀ 𝓑 ⊀')

    h-is-hom : is-Οƒ-suplat-hom 𝓐 𝓐 h
    h-is-hom = ∘-Οƒ-suplat-hom 𝓐 𝓑 𝓐 (Οƒ-rec 𝓑 ⊀') g (Οƒ-rec-is-hom 𝓑 ⊀') g-is-hom

    H : h ＝ id
    H = at-most-one-hom 𝓐 ⊀ h id h-is-hom (id-is-Οƒ-suplat-hom 𝓐) h⊀ refl

    Ξ΄ : (a : A) β†’ P (h a)
    Ξ΄ a = prβ‚‚ (Οƒ-rec 𝓑 ⊀' a)

    Ξ³ : (a : A) β†’ P a
    Ξ³ a = transport P (happly H a) (Ξ΄ a)

\end{code}

For example, we see that the generator ⊀ is the maximum element by
Οƒ-induction:

\begin{code}

  ⊀-is-maximum : (a : A) β†’ a ≀ ⊀
  ⊀-is-maximum = Οƒ-induction
                  (_≀ ⊀)
                  (Ξ» a β†’ ⟨ 𝓐 ⟩-order-is-prop-valued a ⊀)
                  (⟨ 𝓐 ⟩-refl ⊀)
                  (⟨ 𝓐 ⟩-βŠ₯-is-minimum ⊀)
                  (Ξ» a β†’ ⟨ 𝓐 ⟩-⋁-is-lb-of-ubs a ⊀)
\end{code}

We use the following little lemma a couple of times:

\begin{code}

  ⋁-⊀ : (a : β„• β†’ A) (n : β„•) β†’ a n ＝ ⊀ β†’ ⋁ a ＝ ⊀
  ⋁-⊀ a n p = ⟨ 𝓐 ⟩-antisym (⋁ a) ⊀
                   (⊀-is-maximum (⋁ a))
                   (⟨ 𝓐 ⟩-trans ⊀ (a n) (⋁ a)
                          (⟨ 𝓐 ⟩-＝-gives-≀ (p ⁻¹))
                          (⟨ 𝓐 ⟩-⋁-is-ub a n))
\end{code}

We now characterize Οƒ-rec as a least upper bound, or join. We first
define joins and their basic properties:

\begin{code}

  join-of : (𝓑 : Οƒ-SupLat π“₯ 𝓦) {I : 𝓦' Μ‡ } β†’ (I β†’ ⟨ 𝓑 ⟩) β†’ ⟨ 𝓑 ⟩ β†’ π“₯ βŠ” 𝓦 βŠ” 𝓦' Μ‡
  join-of 𝓑 f x = (βˆ€ i β†’ f i β‰€βŸ¨ 𝓑 ⟩ x)
                Γ— ((u : ⟨ 𝓑 ⟩) β†’ (βˆ€ i β†’ f i β‰€βŸ¨ 𝓑 ⟩ u) β†’ x β‰€βŸ¨ 𝓑 ⟩ u)

  syntax join-of 𝓑 f x = x is-the-join-of f on 𝓑

  being-join-is-prop : (𝓑 : Οƒ-SupLat π“₯ 𝓦)
                       {I : 𝓦' Μ‡ }
                       (x : ⟨ 𝓑 ⟩)
                       (f : I β†’ ⟨ 𝓑 ⟩)
                     β†’ is-prop (x is-the-join-of f on 𝓑)
  being-join-is-prop 𝓑 x f = Γ—-is-prop
                              (Ξ -is-prop fe
                                (Ξ» i β†’ ⟨ 𝓑 ⟩-order-is-prop-valued (f i) x))
                              (Ξ β‚‚-is-prop fe
                                (Ξ» u _ β†’ ⟨ 𝓑 ⟩-order-is-prop-valued x u))

  at-most-one-join : (𝓑 : Οƒ-SupLat π“₯ 𝓦)
                     {I : 𝓦' Μ‡ }
                     (x x' : ⟨ 𝓑 ⟩)
                     (f : I β†’ ⟨ 𝓑 ⟩)
                   β†’ x  is-the-join-of f on 𝓑
                   β†’ x' is-the-join-of f on 𝓑
                   β†’ x ＝ x'
  at-most-one-join 𝓑 x x' f (Ξ± , Ξ²) (Ξ±' , Ξ²') =
   ⟨ 𝓑 ⟩-antisym x x' (Ξ² x' Ξ±') (Ξ²' x Ξ±)

\end{code}

We have that the following characterization of (Οƒ-rec 𝓑 t a) as the
least upper bound of the weakly constant family Ξ» (_ : a ＝ ⊀) β†’ t:

\begin{code}

  Οƒ-rec-is-join : (𝓑 : Οƒ-SupLat π“₯ 𝓦) (t : ⟨ 𝓑 ⟩) (a : A)
                β†’ (Οƒ-rec 𝓑 t a) is-the-join-of (Ξ» (_ : a ＝ ⊀) β†’ t) on 𝓑
  Οƒ-rec-is-join 𝓑 t a = Ξ± , Ξ²
   where
    h : A β†’ ⟨ 𝓑 ⟩
    h = Οƒ-rec 𝓑 t

    Ξ± : a ＝ ⊀ β†’ t β‰€βŸ¨ 𝓑 ⟩ h a
    Ξ± p = ⟨ 𝓑 ⟩-＝-gives-≀ (t    ＝⟨ (Οƒ-rec-⊀ 𝓑 t)⁻¹ ⟩
                            h ⊀ ＝⟨ ap (h) (p ⁻¹) ⟩
                            h a ∎)

    Ξ² : (u : ⟨ 𝓑 ⟩) β†’ (a ＝ ⊀ β†’ t β‰€βŸ¨ 𝓑 ⟩ u) β†’ h a β‰€βŸ¨ 𝓑 ⟩ u
    Ξ² = Οƒ-induction
         (Ξ» a β†’ (u : ⟨ 𝓑 ⟩) β†’ (a ＝ ⊀ β†’ t β‰€βŸ¨ 𝓑 ⟩ u) β†’ h a β‰€βŸ¨ 𝓑 ⟩ u)
         (Ξ» a β†’ Ξ β‚‚-is-prop fe (Ξ» u p β†’ ⟨ 𝓑 ⟩-order-is-prop-valued (h a) u))
         β⊀
         Ξ²βŠ₯
         β⋁
         a
     where
      β⊀ : (u : ⟨ 𝓑 ⟩) β†’ (⊀ ＝ ⊀ β†’ t β‰€βŸ¨ 𝓑 ⟩ u) β†’ h ⊀ β‰€βŸ¨ 𝓑 ⟩ u
      β⊀ u Ο† = transport
                (Ξ» - β†’ - β‰€βŸ¨ 𝓑 ⟩ u)
                ((Οƒ-rec-⊀ 𝓑 t )⁻¹)
                (Ο† refl)

      Ξ²βŠ₯ : (u : ⟨ 𝓑 ⟩) β†’ (βŠ₯ ＝ ⊀ β†’ t β‰€βŸ¨ 𝓑 ⟩ u) β†’ h βŠ₯ β‰€βŸ¨ 𝓑 ⟩ u
      Ξ²βŠ₯ u Ο† = transport
                (Ξ» - β†’ - β‰€βŸ¨ 𝓑 ⟩ u)
                ((Οƒ-rec-βŠ₯ 𝓑 t)⁻¹)
                (⟨ 𝓑 ⟩-βŠ₯-is-minimum u)

      β⋁ : (c : β„• β†’ A)
         β†’ ((n : β„•) (u : ⟨ 𝓑 ⟩) β†’ (c n ＝ ⊀ β†’ t β‰€βŸ¨ 𝓑 ⟩ u) β†’ h (c n) β‰€βŸ¨ 𝓑 ⟩ u)
         β†’ (u : ⟨ 𝓑 ⟩) β†’ (⋁ c ＝ ⊀ β†’ t β‰€βŸ¨ 𝓑 ⟩ u) β†’ h (⋁ c) β‰€βŸ¨ 𝓑 ⟩ u
      β⋁ c ψ u Ο† = transport (Ξ» - β†’ - β‰€βŸ¨ 𝓑 ⟩ u) ((Οƒ-rec-⋁ 𝓑 t c)⁻¹) Ξ³
       where
        Ξ³ : β‹βŸ¨ 𝓑 ⟩ (h ∘ c) β‰€βŸ¨ 𝓑 ⟩ u
        Ξ³ = ⟨ 𝓑 ⟩-⋁-is-lb-of-ubs
                 (h ∘ c)
                 u
                 (Ξ» n β†’ ψ n u (Ξ» (p : c n ＝ ⊀) β†’ Ο† (⋁-⊀ c n p)))


  Οƒ-rec-is-ub : (𝓑 : Οƒ-SupLat π“₯ 𝓦) (t : ⟨ 𝓑 ⟩) (a : A)
              β†’ a ＝ ⊀ β†’ t β‰€βŸ¨ 𝓑 ⟩ Οƒ-rec 𝓑 t a
  Οƒ-rec-is-ub 𝓑 t a = pr₁ (Οƒ-rec-is-join 𝓑 t a)

  Οƒ-rec-is-lb-of-ubs : (𝓑 : Οƒ-SupLat π“₯ 𝓦) (t : ⟨ 𝓑 ⟩) (a : A)
                     β†’ (u : ⟨ 𝓑 ⟩) β†’ (a ＝ ⊀ β†’ t β‰€βŸ¨ 𝓑 ⟩ u) β†’ Οƒ-rec 𝓑 t a β‰€βŸ¨ 𝓑 ⟩ u
  Οƒ-rec-is-lb-of-ubs 𝓑 t a = prβ‚‚ (Οƒ-rec-is-join 𝓑 t a)

\end{code}

Such joins are absolute, in the sense that they are preserved by all homomorphisms:

\begin{code}

  Οƒ-suplat-homs-preserve-Οƒ-rec : (𝓑 : Οƒ-SupLat π“₯ 𝓦)
                                 (𝓒 : Οƒ-SupLat 𝓣' π“₯')
                                 (f : ⟨ 𝓑 ⟩ β†’ ⟨ 𝓒 ⟩)
                               β†’ is-Οƒ-suplat-hom 𝓑 𝓒 f
                               β†’ (t : ⟨ 𝓑 ⟩)
                                 (a : A)
                               β†’ f (Οƒ-rec 𝓑 t a) ＝ Οƒ-rec 𝓒 (f t) a
  Οƒ-suplat-homs-preserve-Οƒ-rec 𝓑 𝓒 f i t = happly Ξ³
   where
    composite-is-hom : is-Οƒ-suplat-hom 𝓐 𝓒 (f ∘ Οƒ-rec 𝓑 t)
    composite-is-hom = ∘-Οƒ-suplat-hom 𝓐 𝓑 𝓒 (Οƒ-rec 𝓑 t) f (Οƒ-rec-is-hom 𝓑 t) i

    Ξ³ : f ∘ Οƒ-rec 𝓑 t ＝ Οƒ-rec 𝓒 (f t)
    Ξ³ = at-most-one-hom 𝓒 (f t)
         (f ∘ Οƒ-rec 𝓑 t)
         (Οƒ-rec 𝓒 (f t))
         composite-is-hom
         (Οƒ-rec-is-hom 𝓒 (f t))
         (ap f (Οƒ-rec-⊀ 𝓑 t))
         (Οƒ-rec-⊀ 𝓒 (f t))

\end{code}

In particular, Οƒ-rec preserves Οƒ-rec:

\begin{code}

  Οƒ-rec-preserves-Οƒ-rec : (𝓑 : Οƒ-SupLat π“₯ 𝓦) (t : ⟨ 𝓑 ⟩) (a b : A)
                        β†’ Οƒ-rec 𝓑 t (Οƒ-rec 𝓐 a b) ＝ Οƒ-rec 𝓑 (Οƒ-rec 𝓑 t a) b
  Οƒ-rec-preserves-Οƒ-rec 𝓑 t a b = Οƒ-suplat-homs-preserve-Οƒ-rec 𝓐 𝓑
                                   (Οƒ-rec 𝓑 t) (Οƒ-rec-is-hom 𝓑 t) a b
\end{code}

We now derive the existence of binary meets in the initial
Οƒ-sup-lattice 𝓐 from the above kind of joins.

\begin{code}

  _∧_ : A β†’ A β†’ A
  a ∧ b = Οƒ-rec 𝓐 a b

  meet⊀ : (a : A) β†’ a ∧ ⊀ ＝ a
  meet⊀ = Οƒ-rec-⊀ 𝓐

  meetβŠ₯ : (a : A) β†’ a ∧ βŠ₯ ＝ βŠ₯
  meetβŠ₯ = Οƒ-rec-βŠ₯ 𝓐

  meet⋁ : (a : A) (b : β„• β†’ A) β†’ a ∧ ⋁ b ＝ ⋁ (n ↦ a ∧ b n)
  meet⋁ = Οƒ-rec-⋁ 𝓐

  infix 100 _∧_

  ∧-associative : (a b c : A) β†’ a ∧ (b ∧ c) ＝ (a ∧ b) ∧ c
  ∧-associative = Οƒ-rec-preserves-Οƒ-rec 𝓐

  ∧-is-lb-left : (a b : A) β†’ a ∧ b ≀ a
  ∧-is-lb-left a b = Οƒ-rec-is-lb-of-ubs 𝓐 a b a
                      (Ξ» (_ : b ＝ ⊀) β†’ ⟨ 𝓐 ⟩-refl a)

  ∧-is-lb-right : (a b : A) β†’ a ∧ b ≀ b
  ∧-is-lb-right a b = Οƒ-rec-is-lb-of-ubs 𝓐 a b b
                       (Ξ» (r : b ＝ ⊀) β†’ transport (a ≀_) (r ⁻¹) (⊀-is-maximum a))

\end{code}

Using this, we show that a ∧ b is the greatest lower bound of a and b.
One step needs Οƒ-induction:

\begin{code}

  ∧-is-ub-of-lbs : (a b c : A) β†’ c ≀ a β†’ c ≀ b β†’ c ≀ a ∧ b
  ∧-is-ub-of-lbs a b = Οƒ-induction
                        (Ξ» c β†’ c ≀ a β†’ c ≀ b β†’ c ≀ a ∧ b)
                        (Ξ» c β†’ Ξ β‚‚-is-prop fe
                                 (Ξ» _ _ β†’ ⟨ 𝓐 ⟩-order-is-prop-valued c (a ∧ b)))
                        p⊀
                        pβŠ₯
                        p⋁
   where
    p⊀ : ⊀ ≀ a β†’ ⊀ ≀ b β†’ ⊀ ≀ a ∧ b
    p⊀ l m = ⟨ 𝓐 ⟩-trans _ _ _ l ii
     where
      i : b ＝ ⊀
      i = ⟨ 𝓐 ⟩-antisym _ _ (⊀-is-maximum b) m

      ii : a ≀ a ∧ b
      ii = Οƒ-rec-is-ub 𝓐 a b i

    pβŠ₯ : βŠ₯ ≀ a β†’ βŠ₯ ≀ b β†’ βŠ₯ ≀ a ∧ b
    pβŠ₯ _ _ = ⟨ 𝓐 ⟩-βŠ₯-is-minimum (a ∧ b)

    p⋁ : (d : β„• β†’ A)
       β†’ ((n : β„•) β†’ d n ≀ a β†’ d n ≀ b β†’ d n ≀ a ∧ b)
       β†’ ⋁ d ≀ a
       β†’ ⋁ d ≀ b
       β†’ ⋁ d ≀ (a ∧ b)
    p⋁ d Ο† l m = ⟨ 𝓐 ⟩-⋁-is-lb-of-ubs d (a ∧ b)
                      (Ξ» n β†’ Ο† n (⟨ 𝓐 ⟩-trans (d n) _ a (⟨ 𝓐 ⟩-⋁-is-ub d n) l)
                                 (⟨ 𝓐 ⟩-trans (d n) _ b (⟨ 𝓐 ⟩-⋁-is-ub d n) m))

  ∧-idempotent : (a : A) β†’ a ∧ a ＝ a
  ∧-idempotent a = ⟨ 𝓐 ⟩-antisym _ _ l m
   where
    l : a ∧ a ≀ a
    l = ∧-is-lb-left a a

    m : a ≀ a ∧ a
    m = ∧-is-ub-of-lbs a a a (⟨ 𝓐 ⟩-refl a) (⟨ 𝓐 ⟩-refl a)

  ∧-commutative : (a b : A) β†’ a ∧ b ＝ b ∧ a
  ∧-commutative a b = ⟨ 𝓐 ⟩-antisym _ _ (l a b) (l b a)
   where
    l : (a b : A) β†’ a ∧ b ≀ b ∧ a
    l a b = ∧-is-ub-of-lbs b a (a ∧ b) (∧-is-lb-right a b) (∧-is-lb-left a b)

\end{code}

The intrinsic order coincides with the ∧-semilattice order:

\begin{code}

  from-≀ : (a b : A) β†’ a ≀ b β†’ a ∧ b ＝ a
  from-≀ a b l = ⟨ 𝓐 ⟩-antisym _ _ (∧-is-lb-left a b) m
   where
    m : a ≀ a ∧ b
    m = ∧-is-ub-of-lbs _ _ _ (⟨ 𝓐 ⟩-refl a) l

  to-≀ : (a b : A) β†’ a ∧ b ＝ a β†’ a ≀ b
  to-≀ a b p = ⟨ 𝓐 ⟩-trans _ _ _ l (∧-is-lb-right a b)
   where
    l : a ≀ a ∧ b
    l = ⟨ 𝓐 ⟩-＝-gives-≀ (p ⁻¹)

\end{code}

We now show that the the Οƒ-suplat on one generator is also the initial
Οƒ-frame. The following renaming is annoying.

\begin{code}
  open OrderedTypes.sigma-frame fe
        hiding (order)
        renaming
         (⟨_⟩ to ⟨_⟩' ;
          βŠ₯⟨_⟩ to βŠ₯⟨_⟩' ;
          ⊀⟨_⟩ to ⊀⟨_⟩' ;
          meet to meet' ;
          β‹βŸ¨_⟩ to β‹βŸ¨_⟩' ;
          ⟨_⟩-is-set to ⟨_⟩'-is-set ;
          ⟨_⟩-refl to ⟨_⟩'-refl ;
          ⟨_⟩-trans to ⟨_⟩'-trans ;
          ⟨_⟩-antisym to ⟨_⟩'-antisym ;
          ⟨_⟩-⊀-maximum to ⟨_⟩'-⊀-maximum ;
          ⟨_⟩-βŠ₯-minimum to ⟨_⟩'-βŠ₯-minimum ;
          ⟨_⟩-⋁-is-ub to ⟨_⟩'-⋁-is-ub ;
          ⟨_⟩-⋁-is-lb-of-ubs to ⟨_⟩'-⋁-is-lb-of-ubs)

  𝓐-qua-Οƒ-frame : Οƒ-Frame 𝓣
  𝓐-qua-Οƒ-frame = A ,
                  (⊀ , _∧_ , βŠ₯ , ⋁) ,
                  ⟨ 𝓐 ⟩-is-set ,
                  ∧-idempotent ,
                  ∧-commutative ,
                  ∧-associative ,
                  (Ξ» a β†’ ∧-commutative βŠ₯ a βˆ™ meetβŠ₯ a) ,
                  meet⊀ ,
                  meet⋁ ,
                  (Ξ» a n β†’ from-≀ (a n) (⋁ a)
                            (⟨ 𝓐 ⟩-⋁-is-ub a n)) ,
                  (Ξ» a u Ο† β†’ from-≀ (⋁ a) u
                              (⟨ 𝓐 ⟩-⋁-is-lb-of-ubs a u
                                    (Ξ» n β†’ to-≀ (a n) u (Ο† n))))

  𝓐-qua-Οƒ-frame-is-initial : (𝓑 : Οƒ-Frame π“₯)
                           β†’ βˆƒ! f κž‰ (A β†’ ⟨ 𝓑 ⟩), is-Οƒ-frame-hom 𝓐-qua-Οƒ-frame 𝓑 f
  𝓐-qua-Οƒ-frame-is-initial {π“₯} 𝓑 = Ξ³
   where
    B = ⟨ 𝓑 ⟩

    _∧'_ : B β†’ B β†’ B
    _∧'_ = meet' 𝓑

    𝓑-qua-Οƒ-suplat : Οƒ-SupLat π“₯ π“₯
    𝓑-qua-Οƒ-suplat = Οƒ-frames-are-Οƒ-suplats 𝓑

    ⊀' : B
    ⊀' = ⊀⟨ 𝓑 ⟩'

    f : A β†’ B
    f = Οƒ-rec 𝓑-qua-Οƒ-suplat ⊀'

    f-is-hom : is-Οƒ-suplat-hom 𝓐 𝓑-qua-Οƒ-suplat f
    f-is-hom = Οƒ-rec-is-hom 𝓑-qua-Οƒ-suplat ⊀'

    f-preserves-∧ : (a b : A) β†’ f (a ∧ b) ＝ f a ∧' f b
    f-preserves-∧ a = Οƒ-induction
                       (Ξ» b β†’ f (a ∧ b) ＝ f a ∧' f b)
                       (Ξ» b β†’ ⟨ 𝓑 ⟩'-is-set)
                       f⊀
                       fβŠ₯
                       f⋁
     where
      f⊀ = f (a ∧ ⊀)  ＝⟨ I ⟩
           f a        ＝⟨ II ⟩
           f a ∧' ⊀'  ＝⟨ III ⟩
           f a ∧' f ⊀ ∎
            where
             I   = ap f (meet⊀ a)
             II  = (⟨ 𝓑 ⟩'-⊀-maximum (f a))⁻¹
             III = ap (f a ∧'_) ((Οƒ-rec-⊀ 𝓑-qua-Οƒ-suplat ⊀')⁻¹)

      fβŠ₯ = f (a ∧ βŠ₯)      ＝⟨ I ⟩
           f βŠ₯            ＝⟨ II ⟩
           βŠ₯⟨ 𝓑 ⟩'        ＝⟨ III ⟩
           βŠ₯⟨ 𝓑 ⟩' ∧' f a ＝⟨ IV ⟩
           f βŠ₯ ∧' f a     ＝⟨ V ⟩
           f a ∧' f βŠ₯     ∎
            where
             I   = ap f (meetβŠ₯ a)
             II  = Οƒ-suplat-hom-βŠ₯ 𝓐 𝓑-qua-Οƒ-suplat f f-is-hom
             III = (⟨ 𝓑 ⟩'-βŠ₯-minimum (f a))⁻¹
             IV  = ap (Ξ» - β†’ - ∧' f a)
                      ((Οƒ-suplat-hom-βŠ₯ 𝓐 𝓑-qua-Οƒ-suplat f f-is-hom)⁻¹)
             V   = ⟨ 𝓑 ⟩-commutativity (f βŠ₯) (f a)

      f⋁ = Ξ» c p β†’
           f (a ∧ ⋁ c)                    ＝⟨ I c ⟩
           f (⋁ (n ↦ a ∧ c n))            ＝⟨ II c ⟩
           β‹βŸ¨ 𝓑 ⟩' (n ↦ f (a ∧ c n))      ＝⟨ III c p ⟩
           β‹βŸ¨ 𝓑 ⟩' (n ↦ f a ∧' f (c n))   ＝⟨ IV c ⟩
           f a ∧' β‹βŸ¨ 𝓑 ⟩' (Ξ» n β†’ f (c n)) ＝⟨ V c ⟩
           f a ∧' f (⋁ c)                 ∎
            where
             I   = Ξ» c β†’ ap f (meet⋁ a c)
             II  = Ξ» c β†’ Οƒ-suplat-hom-⋁
                          𝓐
                          𝓑-qua-Οƒ-suplat
                          f
                          f-is-hom
                          (Ξ» n β†’ a ∧ c n)
             III = Ξ» c p β†’ ap β‹βŸ¨ 𝓑 ⟩' (dfunext fe p)
             IV  = Ξ» c β†’ (⟨ 𝓑 ⟩-distributivity (f a) (Ξ» n β†’ f (c n)))⁻¹
             V   = Ξ» c β†’ ap (f a ∧'_)
                            ((Οƒ-suplat-hom-⋁ 𝓐 𝓑-qua-Οƒ-suplat f f-is-hom c)⁻¹)

    f-is-hom' : is-Οƒ-frame-hom 𝓐-qua-Οƒ-frame 𝓑 f
    f-is-hom' = Οƒ-rec-⊀ 𝓑-qua-Οƒ-suplat ⊀' ,
                f-preserves-∧ ,
                Οƒ-suplat-hom-βŠ₯ 𝓐 𝓑-qua-Οƒ-suplat f f-is-hom ,
                Οƒ-suplat-hom-⋁ 𝓐 𝓑-qua-Οƒ-suplat f f-is-hom

    forget : (g : A β†’ B)
           β†’ is-Οƒ-frame-hom  𝓐-qua-Οƒ-frame 𝓑              g
           β†’ is-Οƒ-suplat-hom 𝓐             𝓑-qua-Οƒ-suplat g
    forget g (i , ii , iii , iv) = (iii , iv)

    f-uniqueness : (g : A β†’ B) β†’ is-Οƒ-frame-hom 𝓐-qua-Οƒ-frame 𝓑 g β†’ f ＝ g
    f-uniqueness g g-is-hom' = at-most-one-hom 𝓑-qua-Οƒ-suplat ⊀' f g
                                f-is-hom
                                (forget g g-is-hom')
                                (Οƒ-rec-⊀ 𝓑-qua-Οƒ-suplat ⊀')
                                (Οƒ-frame-hom-⊀ 𝓐-qua-Οƒ-frame 𝓑 g g-is-hom')

    Ξ³ : βˆƒ! f κž‰ (A β†’ B), is-Οƒ-frame-hom 𝓐-qua-Οƒ-frame 𝓑 f
    Ξ³ = (f , f-is-hom') ,
        (Ξ» (g , g-is-hom') β†’ to-subtype-＝
                              (being-Οƒ-frame-hom-is-prop 𝓐-qua-Οƒ-frame 𝓑)
                              (f-uniqueness g g-is-hom'))
\end{code}

We now regard the type of propositions as a Οƒ-sup-lattice:

\begin{code}

  Ξ©-qua-Οƒ-Frame : Οƒ-Frame (𝓣 ⁺)
  Ξ©-qua-Οƒ-Frame = OrderedTypes.sigma-frame.Ξ©-qua-Οƒ-frame fe pe pt

  Ξ©-qua-Οƒ-SupLat : Οƒ-SupLat (𝓣 ⁺) (𝓣 ⁺)
  Ξ©-qua-Οƒ-SupLat = OrderedTypes.sigma-frame.Ξ©-qua-Οƒ-suplat fe pe pt

  private
   βŠ₯'   = βŠ₯⟨ Ξ©-qua-Οƒ-SupLat ⟩
   ⊀'   = ⊀⟨ Ξ©-qua-Οƒ-Frame ⟩'
   ⋁'  = β‹βŸ¨ Ξ©-qua-Οƒ-SupLat ⟩
   _≀'_ : Ξ© 𝓣 β†’ Ξ© 𝓣 β†’ 𝓣 ⁺ Μ‡
   x ≀' y = x β‰€βŸ¨ Ξ©-qua-Οƒ-SupLat ⟩ y

   ＝-gives-≀' : (p q : Ξ© 𝓣) β†’ p ＝ q β†’ p ≀' q
   ＝-gives-≀' p q r = ⟨ Ξ©-qua-Οƒ-SupLat ⟩-＝-gives-≀ r

\end{code}

In a frame the bottom element is not taken explicitly as part of the
structure and is defined to be the join of the family indexed by the
empty set. In the particular case of the frame of propositions, this
is equal to the empty type 𝟘, but not definitionally:

\begin{code}

  βŠ₯-holds-is-𝟘 : βŠ₯' holds ＝ 𝟘
  βŠ₯-holds-is-𝟘 = p
   where
    p : (βˆƒ x κž‰ 𝟘 , unique-from-𝟘 x holds) ＝ 𝟘
    p = pe βˆƒ-is-prop
           𝟘-is-prop
           (βˆ₯βˆ₯-rec 𝟘-is-prop (unique-from-𝟘 ∘ pr₁))
           unique-from-𝟘

  Ξ©-non-trivial : βŠ₯' β‰  ⊀'
  Ξ©-non-trivial q = 𝟘-is-not-πŸ™ r
   where
    r : 𝟘 ＝ πŸ™
    r = (βŠ₯-holds-is-𝟘)⁻¹ βˆ™ ap _holds q

\end{code}

The following map Ο„ will play an important role:

\begin{code}

  Ο„ : A β†’ Ξ© 𝓣
  Ο„ = Οƒ-rec Ξ©-qua-Οƒ-SupLat ⊀'

  Ο„-is-hom : is-Οƒ-suplat-hom 𝓐 Ξ©-qua-Οƒ-SupLat Ο„
  Ο„-is-hom = Οƒ-rec-is-hom Ξ©-qua-Οƒ-SupLat ⊀'

\end{code}

Using Ο„ we derive the non-triviality of 𝓐 from that of Ξ©:

\begin{code}

  𝓐-non-trivial : βŠ₯ β‰  ⊀
  𝓐-non-trivial p = Ξ©-non-trivial q
   where
    q = βŠ₯'  ＝⟨ (Οƒ-suplat-hom-βŠ₯ 𝓐 Ξ©-qua-Οƒ-SupLat Ο„ Ο„-is-hom)⁻¹ ⟩
        Ο„ βŠ₯ ＝⟨ ap Ο„ p ⟩
        Ο„ ⊀ ＝⟨ Οƒ-rec-⊀ Ξ©-qua-Οƒ-SupLat ⊀' ⟩
        ⊀'  ∎

\end{code}

A crucial property of the map Ο„ is that it reflects top elements (in
point-free topological terms, this says that Ο„ is dense):

\begin{code}

  Ο„-reflects-⊀ : (a : A) β†’ Ο„ a ＝ ⊀' β†’ a ＝ ⊀
  Ο„-reflects-⊀ = Οƒ-induction
                  (Ξ» a β†’ Ο„ a ＝ ⊀' β†’ a ＝ ⊀)
                  (Ξ» a β†’ Ξ -is-prop fe (Ξ» _ β†’ ⟨ 𝓐 ⟩-is-set))
                  i⊀
                  iβŠ₯
                  i⋁
   where
    i⊀ : Ο„ ⊀ ＝ ⊀' β†’ ⊀ ＝ ⊀
    i⊀ _ = refl

    iβŠ₯ : Ο„ βŠ₯ ＝ ⊀' β†’ βŠ₯ ＝ ⊀
    iβŠ₯ p = 𝟘-elim (Ξ©-non-trivial q)
     where
      q : βŠ₯' ＝ ⊀'
      q = (Οƒ-suplat-hom-βŠ₯ 𝓐 Ξ©-qua-Οƒ-SupLat Ο„ Ο„-is-hom)⁻¹ βˆ™ p

    i⋁ : (a : β„• β†’ A)
       β†’ ((n : β„•) β†’ Ο„ (a n) ＝ ⊀' β†’ a n ＝ ⊀)
       β†’ Ο„ (⋁ a) ＝ ⊀'
       β†’ ⋁ a ＝ ⊀
    i⋁ a Ο† p = βˆ₯βˆ₯-rec ⟨ 𝓐 ⟩-is-set iii ii
     where
      i : ⋁' (Ο„ ∘ a) ＝ ⊀'
      i = (Οƒ-suplat-hom-⋁ 𝓐 Ξ©-qua-Οƒ-SupLat Ο„ Ο„-is-hom a)⁻¹ βˆ™ p

      ii : βˆƒ n κž‰ β„• , Ο„ (a n) holds
      ii = equal-⊀-gives-holds (⋁' (Ο„ ∘ a)) i

      iii : (Ξ£ n κž‰ β„• , Ο„ (a n) holds) β†’ ⋁ a ＝ ⊀
      iii (n , h) = vi
       where
        iv : Ο„ (a n) ＝ ⊀'
        iv = holds-gives-equal-⊀ pe fe (Ο„ (a n)) h

        v : a n ＝ ⊀
        v = Ο† n iv

        vi : ⋁ a ＝ ⊀
        vi = ⋁-⊀ a n v

\end{code}

A frame is called compact if every cover of its top element has a
finite subcover. It is supercompact (I think the terminology is due to
John Isbell) if every cover of the top element has a singleton
subcover. This motivates the name of the following theorem, whose
crucial ingredient is the homomorphism Ο„ and the fact that it reflects
top elements.

\begin{code}

  𝓐-is-Οƒ-super-compact : (a : β„• β†’ A) β†’ ⋁ a ＝ ⊀ β†’ βˆƒ n κž‰ β„• , a n ＝ ⊀
  𝓐-is-Οƒ-super-compact a p = vi
   where
    i = ⋁' (Ο„ ∘ a) ＝⟨ (Οƒ-suplat-hom-⋁ 𝓐 Ξ©-qua-Οƒ-SupLat Ο„ Ο„-is-hom a)⁻¹ ⟩
        Ο„ (⋁ a)    ＝⟨ ap Ο„ p ⟩
        Ο„ ⊀        ＝⟨ Οƒ-rec-⊀ Ξ©-qua-Οƒ-SupLat ⊀' ⟩
        ⊀'         ∎

    ii : (βˆƒ n κž‰ β„• , Ο„ (a n) holds) ＝ πŸ™
    ii = ap _holds i

    iii : (Ξ£ n κž‰ β„• , Ο„ (a n) holds) β†’ (Ξ£ n κž‰ β„• , a n ＝ ⊀)
    iii (n , h) = n , v
     where
      iv : Ο„ (a n) ＝ ⊀'
      iv = holds-gives-equal-⊀ pe fe (Ο„ (a n)) h

      v : a n ＝ ⊀
      v = Ο„-reflects-⊀ (a n) iv

    vi : βˆƒ n κž‰ β„• , a n ＝ ⊀
    vi = βˆ₯βˆ₯-functor iii (equal-πŸ™-gives-holds (βˆƒ n κž‰ β„• , Ο„ (a n) holds) ii)

\end{code}

We have that Ο„ a holds precisely when a ＝ ⊀ (hence the name Ο„ for the
function):

\begin{code}

  Ο„-characβ†’ : (a : A) β†’ Ο„ a holds β†’ a ＝ ⊀
  Ο„-characβ†’ a h = Ο„-reflects-⊀ a (holds-gives-equal-⊀ pe fe (Ο„ a) h)

  Ο„-charac← : (a : A) β†’ a ＝ ⊀ β†’ Ο„ a holds
  Ο„-charac← a p = equal-⊀-gives-holds (Ο„ a)
                   (Ο„ a ＝⟨ ap Ο„ p ⟩
                    Ο„ ⊀ ＝⟨ Οƒ-rec-⊀ Ξ©-qua-Οƒ-SupLat ⊀' ⟩
                    ⊀'  ∎)

  Ο„-charac' : (a : A) β†’ Ο„ a holds ＝ (a ＝ ⊀)
  Ο„-charac' a = pe (holds-is-prop (Ο„ a)) ⟨ 𝓐 ⟩-is-set (Ο„-characβ†’ a) (Ο„-charac← a)

  Ο„-charac : (a : A) β†’ Ο„ a ＝ ((a ＝ ⊀) , ⟨ 𝓐 ⟩-is-set)
  Ο„-charac a = to-subtype-＝ (Ξ» a β†’ being-prop-is-prop fe) (Ο„-charac' a)

\end{code}

The following criterion for a ≀ b will be useful:

\begin{code}

  ≀-criterion : (a b : A) β†’ (a ＝ ⊀ β†’ b ＝ ⊀) β†’ a ≀ b
  ≀-criterion = Οƒ-induction
                  (Ξ» a β†’ (b : A) β†’ (a ＝ ⊀ β†’ b ＝ ⊀) β†’ a ≀ b)
                  (Ξ» a β†’ Ξ β‚‚-is-prop fe (Ξ» b _ β†’ ⟨ 𝓐 ⟩-order-is-prop-valued a b))
                  i⊀
                  iβŠ₯
                  i⋁
   where
    i⊀ : (b : A) β†’ (⊀ ＝ ⊀ β†’ b ＝ ⊀) β†’ ⊀ ≀ b
    i⊀ b f = ⟨ 𝓐 ⟩-＝-gives-≀ ((f refl)⁻¹)

    iβŠ₯ : (b : A) β†’ (βŠ₯ ＝ ⊀ β†’ b ＝ ⊀) β†’ βŠ₯ ≀ b
    iβŠ₯ b _ = ⟨ 𝓐 ⟩-βŠ₯-is-minimum b

    i⋁ : (a : β„• β†’ A)
       β†’ ((n : β„•) (b : A) β†’ (a n ＝ ⊀ β†’ b ＝ ⊀) β†’ a n ≀ b)
       β†’ (b : A)
       β†’ (⋁ a ＝ ⊀ β†’ b ＝ ⊀)
       β†’ ⋁ a ≀ b
    i⋁ a Ο† b ψ = ⟨ 𝓐 ⟩-⋁-is-lb-of-ubs a b
                      (Ξ» n β†’ Ο† n b (Ξ» (p : a n ＝ ⊀) β†’ ψ (⋁-⊀ a n p)))

  ≀-criterion-converse : (a b : A) β†’ a ≀ b β†’ (a ＝ ⊀ β†’ b ＝ ⊀)
  ≀-criterion-converse a b l p =
   ⟨ 𝓐 ⟩-antisym _ _
        (⊀-is-maximum b)
        (⟨ 𝓐 ⟩-trans _ _ _ (⟨ 𝓐 ⟩-＝-gives-≀ (p ⁻¹)) l)

\end{code}

The map Ο„ reflects order and hence is left-cancellable, and therefore
is an embedding (its fibers are propositions) because it is a map into
a set:

\begin{code}

  Ο„-order-lc : (a b : A) β†’ Ο„ a ≀' Ο„ b β†’ a ≀ b
  Ο„-order-lc a b l = iv
   where
    i : Ο„ a holds β†’ Ο„ b holds
    i = OrderedTypes.Frame.from-≀Ω fe pe pt {𝓣} {Ο„ a} {Ο„ b} l

    ii : Ο„ a ＝ ⊀' β†’ Ο„ b ＝ ⊀'
    ii p = holds-gives-equal-⊀ pe fe (Ο„ b) (i (equal-⊀-gives-holds (Ο„ a) p))

    iii : a ＝ ⊀ β†’ b ＝ ⊀
    iii q = Ο„-reflects-⊀ b (ii r)
     where
      r = Ο„ a ＝⟨ ap Ο„ q ⟩
          Ο„ ⊀ ＝⟨ Οƒ-rec-⊀ Ξ©-qua-Οƒ-SupLat ⊀' ⟩
          ⊀'  ∎

    iv : a ≀ b
    iv = ≀-criterion a b iii

  Ο„-lc : left-cancellable Ο„
  Ο„-lc {a} {b} p = ⟨ 𝓐 ⟩-antisym a b l r
   where
    l : a ≀ b
    l = Ο„-order-lc a b (＝-gives-≀' (Ο„ a) (Ο„ b) p)

    r : b ≀ a
    r = Ο„-order-lc b a (＝-gives-≀' (Ο„ b) (Ο„ a) (p ⁻¹))

  Ο„-is-embedding : is-embedding Ο„
  Ο„-is-embedding = lc-maps-into-sets-are-embeddings Ο„ Ο„-lc (Ξ©-is-set fe pe)

  holds-is-embedding : is-embedding (_holds {𝓣})
  holds-is-embedding = pr₁-is-embedding (Ξ» _ β†’ being-prop-is-prop fe)

\end{code}

Hence the composite Ο„-holds is an embedding of A into the universe 𝓣:

\begin{code}

  Ο„-holds : A β†’ 𝓣 Μ‡
  Ο„-holds a = Ο„ a holds

  Ο„-holds-is-embedding : is-embedding Ο„-holds
  Ο„-holds-is-embedding = ∘-is-embedding Ο„-is-embedding holds-is-embedding

\end{code}

Using this we define the notion of quasidecidability and its required
properties. We define the quasidecidability of the type P to be the
type

  fiber Ο„-holds P,

which amounts to the type

  Ξ£ a κž‰ A , (Ο„ a holds ＝ P)

by construction:

\begin{code}

  is-quasidecidable : 𝓣 Μ‡ β†’ 𝓣 ⁺ Μ‡
  is-quasidecidable P = Ξ£ a κž‰ A , (Ο„ a holds ＝ P)

  being-quasidecidable-is-prop : βˆ€ P β†’ is-prop (is-quasidecidable P)
  being-quasidecidable-is-prop = Ο„-holds-is-embedding

  quasidecidable-types-are-props : βˆ€ P β†’ is-quasidecidable P β†’ is-prop P
  quasidecidable-types-are-props P (a , p) =
   transport is-prop p (holds-is-prop (Ο„ a))

  𝟘-is-quasidecidable : is-quasidecidable 𝟘
  𝟘-is-quasidecidable = βŠ₯ ,
                        (Ο„ βŠ₯ holds ＝⟨ I ⟩
                         βŠ₯' holds  ＝⟨ II ⟩
                         𝟘         ∎)
                          where
                           I  = ap _holds
                                   (Οƒ-suplat-hom-βŠ₯ 𝓐 Ξ©-qua-Οƒ-SupLat Ο„ Ο„-is-hom)
                           II = βŠ₯-holds-is-𝟘

  πŸ™-is-quasidecidable : is-quasidecidable πŸ™
  πŸ™-is-quasidecidable = ⊀ , ap _holds (Οƒ-rec-⊀ Ξ©-qua-Οƒ-SupLat ⊀')

  quasidecidable-closed-under-Ο‰-joins
   : (P : β„• β†’ 𝓣 Μ‡ )
   β†’ ((n : β„•) β†’ is-quasidecidable (P n))
   β†’ is-quasidecidable (βˆƒ n κž‰ β„• , P n)
  quasidecidable-closed-under-Ο‰-joins P Ο† = vii
   where
    i : (n : β„•) β†’ Ο„-holds (fiber-point (Ο† n)) ＝ P n
    i n = fiber-identification (Ο† n)

    ii : (n : β„•)
       β†’ Ο„ (fiber-point (Ο† n)) ＝ P n , quasidecidable-types-are-props (P n) (Ο† n)
    ii n = to-subtype-＝ (Ξ» _ β†’ being-prop-is-prop fe) (i n)

    iii : Ο„ (⋁ (n ↦ fiber-point (Ο† n)))
        ＝ ⋁' (Ξ» n β†’ P n , quasidecidable-types-are-props (P n) (Ο† n))
    iii = Ο„ (⋁ (n ↦ fiber-point (Ο† n)))                               ＝⟨ iv ⟩
          ⋁' (n ↦ Ο„ (fiber-point (Ο† n)))                              ＝⟨ v ⟩
          ⋁' (n ↦ (P n , quasidecidable-types-are-props (P n) (Ο† n))) ∎
     where
      iv = Οƒ-suplat-hom-⋁ 𝓐 Ξ©-qua-Οƒ-SupLat Ο„ Ο„-is-hom (Ξ» n β†’ fiber-point (Ο† n))
      v  = ap ⋁' (dfunext fe ii)

    vi : Ο„-holds (⋁ (n ↦ fiber-point (Ο† n))) ＝ (βˆƒ n κž‰ β„• , P n)
    vi = ap _holds iii

    vii : is-quasidecidable (βˆƒ n κž‰ β„• , P n)
    vii = ⋁ (n ↦ fiber-point (Ο† n)) , vi

\end{code}

Then we get quasidecidable induction by Οƒ-induction:

\begin{code}

  quasidecidable-induction :
     (F : 𝓣 Μ‡ β†’ π“₯ Μ‡ )
   β†’ ((P : 𝓣 Μ‡ ) β†’ is-prop (F P))
   β†’ F 𝟘
   β†’ F πŸ™
   β†’ ((P : β„• β†’ 𝓣 Μ‡ ) β†’ ((n : β„•) β†’ F (P n)) β†’ F (βˆƒ n κž‰ β„• , P n))
   β†’ (P : 𝓣 Μ‡ ) β†’ is-quasidecidable P β†’ F P
  quasidecidable-induction {π“₯} F i Fβ‚€ F₁ FΟ‰ P (a , r) = Ξ³ a P r
   where
    Ξ³ : (a : A) (P : 𝓣 Μ‡ ) β†’ Ο„ a holds ＝ P β†’ F P
    Ξ³ = Οƒ-induction
         (Ξ» a β†’ (P : 𝓣 Μ‡ ) β†’ Ο„ a holds ＝ P β†’ F P)
         (Ξ» a β†’ Ξ β‚‚-is-prop fe (Ξ» P _ β†’ i P))
         γ⊀
         Ξ³βŠ₯
         γ⋁
     where
      γ⊀ : (P : 𝓣 Μ‡ ) β†’ Ο„ ⊀ holds ＝ P β†’ F P
      γ⊀ P s = transport F (t ⁻¹ βˆ™ s) F₁
       where
        t : Ο„ ⊀ holds ＝ πŸ™
        t = ap _holds (Οƒ-rec-⊀ Ξ©-qua-Οƒ-SupLat ⊀')

      Ξ³βŠ₯ : (P : 𝓣 Μ‡ ) β†’ Ο„ βŠ₯ holds ＝ P β†’ F P
      Ξ³βŠ₯ P s = transport F (t ⁻¹ βˆ™ s) Fβ‚€
       where
        t : Ο„ βŠ₯ holds ＝ 𝟘
        t = ap _holds (Οƒ-suplat-hom-βŠ₯ 𝓐 Ξ©-qua-Οƒ-SupLat Ο„ Ο„-is-hom) βˆ™ βŠ₯-holds-is-𝟘

      γ⋁ : (a : β„• β†’ A)
         β†’ ((n : β„•) (P : 𝓣 Μ‡ ) β†’ (Ο„ (a n) holds) ＝ P β†’ F P)
         β†’ (P : 𝓣 Μ‡ ) β†’ (Ο„ (⋁ a) holds) ＝ P β†’ F P
      γ⋁ a Ο† P s = transport F (t ⁻¹ βˆ™ s) (FΟ‰ (Ξ» n β†’ Ο„ (a n) holds) ψ)
       where
        t : Ο„ (⋁ a) holds ＝ (βˆƒ n κž‰ β„• , Ο„ (a n) holds)
        t = ap _holds (Οƒ-suplat-hom-⋁ 𝓐 Ξ©-qua-Οƒ-SupLat Ο„ Ο„-is-hom a)
        ψ : (n : β„•) β†’ F (Ο„ (a n) holds)
        ψ n = Ο† n (Ο„ (a n) holds) refl

\end{code}

We then get the dominance axiom for quasidecidable propositions by an
application of the submodule hypothetical-quasidecidability.

\begin{code}

  quasidecidable-closed-under-Ξ£
   : (P : 𝓣 Μ‡ )
   β†’ (Q : P β†’ 𝓣 Μ‡ )
   β†’ is-quasidecidable P
   β†’ ((p : P) β†’ is-quasidecidable (Q p))
   β†’ is-quasidecidable (Ξ£ Q)
  quasidecidable-closed-under-Ξ£ =
   hypothetical-quasidecidability.quasidecidable-closed-under-Ξ£
     (quasidecidable-propositions
        is-quasidecidable
        being-quasidecidable-is-prop
        𝟘-is-quasidecidable
        πŸ™-is-quasidecidable
        quasidecidable-closed-under-Ο‰-joins
        quasidecidable-induction)

\end{code}

Here are some consequences for the sake of illustration of the meaning
of this.

\begin{code}

  dependent-binary-meet
   : (a : A) (b : Ο„ a holds β†’ A)
   β†’ Ξ£ c κž‰ A , (Ο„ c holds) ＝ (Ξ£ h κž‰ Ο„ a holds , Ο„ (b h) holds)
  dependent-binary-meet a b = quasidecidable-closed-under-Ξ£
                               (Ο„ a holds)
                               (Ξ» h β†’ Ο„ (b h) holds)
                               (a , refl)
                               (Ξ» h β†’ b h , refl)
\end{code}

The following just applies back-and-forth the characterization of
Ο„ a holds as a ＝ ⊀.

\begin{code}

  dependent-binary-meet' : (a : A) (b : a ＝ ⊀ β†’ A)
                         β†’ Ξ£ c κž‰ A , (c ＝ ⊀ ↔ (Ξ£ p κž‰ a ＝ ⊀ , b p ＝ ⊀))
  dependent-binary-meet' a b = f Οƒ
   where
    b' : Ο„ a holds β†’ A
    b' h = b (τ-charac→ a h)

    Οƒ : Ξ£ c κž‰ A , (Ο„ c holds) ＝ (Ξ£ h κž‰ Ο„ a holds , Ο„ (b' h) holds)
    Οƒ = dependent-binary-meet a b'

    f : (Ξ£ c κž‰ A , (Ο„ c holds) ＝ (Ξ£ h κž‰ Ο„ a holds , Ο„ (b' h) holds))
      β†’ Ξ£ c κž‰ A , ((c ＝ ⊀) ↔ (Ξ£ p κž‰ a ＝ ⊀ , b p ＝ ⊀))
    f ( c , q) = c , g , h
     where
      g : c ＝ ⊀ β†’ Ξ£ p κž‰ a ＝ ⊀ , b p ＝ ⊀
      g r = Ο„-characβ†’ a (pr₁ (Idtofun q (Ο„-charac← c r))) ,
            transport (Ξ» - β†’ b - ＝ ⊀)
              (⟨ 𝓐 ⟩-is-set _ _)
              (Ο„-characβ†’ (b _) (prβ‚‚ (Idtofun q (Ο„-charac← c r))))

      h : (Ξ£ p κž‰ a ＝ ⊀ , b p ＝ ⊀) β†’ c ＝ ⊀
      h (p , s) = τ-charac→ c
                   (Idtofun
                     (q ⁻¹)
                     (Ο„-charac← a p , Ο„-charac← (b' (Ο„-charac← a p))
                     (transport (Ξ» - β†’ b - ＝ ⊀) (⟨ 𝓐 ⟩-is-set _ _) s)))
\end{code}

We can replace the bi-implication by an equality:

\begin{code}

  dependent-binary-meet'' : (a : A) (b : a ＝ ⊀ β†’ A)
                          β†’ Ξ£ c κž‰ A , ((c ＝ ⊀) ＝ (Ξ£ p κž‰ a ＝ ⊀ , b p ＝ ⊀))
  dependent-binary-meet'' a b = f (dependent-binary-meet' a b)
   where
    f : (Ξ£ c κž‰ A , (c ＝ ⊀ ↔ (Ξ£ p κž‰ a ＝ ⊀ , b p ＝ ⊀)))
      β†’ Ξ£ c κž‰ A , ((c ＝ ⊀) ＝ (Ξ£ p κž‰ a ＝ ⊀ , b p ＝ ⊀))
    f (c , g , h) = c , ⌜ prop-univalent-≃ pe fe (c ＝ ⊀) (Ξ£ p κž‰ a ＝ ⊀ , b p ＝ ⊀)
                           (Ξ£-is-prop ⟨ 𝓐 ⟩-is-set (Ξ» p β†’ ⟨ 𝓐 ⟩-is-set)) ⌝⁻¹
                          (logically-equivalent-props-are-equivalent
                             ⟨ 𝓐 ⟩-is-set
                             (Ξ£-is-prop
                               ⟨ 𝓐 ⟩-is-set
                               (Ξ» p β†’ ⟨ 𝓐 ⟩-is-set)) g h)
\end{code}

The non-dependent special case:

\begin{code}

  binary-meet : (a b : A) β†’ Ξ£ c κž‰ A , (c ＝ ⊀ ↔ ((a ＝ ⊀) Γ— (b ＝ ⊀)))
  binary-meet a b = dependent-binary-meet' a (Ξ» _ β†’ b)

\end{code}

Using the criterion for ≀ we get that this does indeed give binary
meets:

\begin{code}

  binary-meet'-is-∧ : (a b c : A)
                    β†’ (c ＝ ⊀ ↔ ((a ＝ ⊀) Γ— (b ＝ ⊀)))
                    β†’ c ＝ a ∧ b
  binary-meet'-is-∧ a b c (f , g) = viii
   where
    i : c ≀ a
    i = ≀-criterion c a (Ξ» (p : c ＝ ⊀) β†’ pr₁ (f p))

    ii : c ≀ b
    ii = ≀-criterion c b (Ξ» (p : c ＝ ⊀) β†’ prβ‚‚ (f p))

    iii : c ≀ a ∧ b
    iii = ∧-is-ub-of-lbs a b c i ii

    iv : a ∧ b ＝ ⊀ β†’ a ＝ ⊀
    iv p = ⟨ 𝓐 ⟩-antisym a ⊀
                (⊀-is-maximum a)
                (⟨ 𝓐 ⟩-trans ⊀ (a ∧ b) a
                      (⟨ 𝓐 ⟩-＝-gives-≀ (p ⁻¹))
                      (∧-is-lb-left a b))

    v : a ∧ b ＝ ⊀ β†’ b ＝ ⊀
    v p = ⟨ 𝓐 ⟩-antisym b ⊀
               (⊀-is-maximum b)
               (⟨ 𝓐 ⟩-trans ⊀ (a ∧ b) b
                     (⟨ 𝓐 ⟩-＝-gives-≀ (p ⁻¹))
                     (∧-is-lb-right a b))

    vi : a ∧ b ＝ ⊀ β†’ c ＝ ⊀
    vi p = g (iv p , v p)

    vii : a ∧ b ≀ c
    vii = ≀-criterion (a ∧ b) c vi

    viii : c ＝ a ∧ b
    viii = ⟨ 𝓐 ⟩-antisym c (a ∧ b) iii vii

\end{code}

Οƒ-sup-lattices have joins of quasidecidable-indexed families:

\begin{code}

  Οƒ-suplats-have-quasidecidable-joins : (𝓑 : Οƒ-SupLat π“₯ 𝓦) (P : 𝓣 Μ‡ )
                                      β†’ is-quasidecidable P
                                      β†’ (f : P β†’ ⟨ 𝓑 ⟩)
                                      β†’ Ξ£ b κž‰ ⟨ 𝓑 ⟩ , (b is-the-join-of f on 𝓑)
  Οƒ-suplats-have-quasidecidable-joins {π“₯} {𝓦} 𝓑 =
    quasidecidable-induction F F-is-prop-valued Fβ‚€ F₁ FΟ‰
   where
    F : 𝓣 Μ‡ β†’ 𝓣 βŠ” π“₯ βŠ” 𝓦 Μ‡
    F P = (f : P β†’ ⟨ 𝓑 ⟩) β†’ Ξ£ b κž‰ ⟨ 𝓑 ⟩ , (b is-the-join-of f on 𝓑)

    F-is-prop-valued : βˆ€ P β†’ is-prop (F P)
    F-is-prop-valued P = Ξ -is-prop fe
                          (Ξ» f (b , i) (b' , i')
                             β†’ to-subtype-＝
                                (Ξ» b β†’ being-join-is-prop 𝓑 b f)
                                (at-most-one-join 𝓑 b b' f i i'))

    Fβ‚€ : F 𝟘
    Fβ‚€ f = βŠ₯⟨ 𝓑 ⟩ , (Ξ» (i : 𝟘) β†’ 𝟘-elim i) , Ξ» u ψ β†’ ⟨ 𝓑 ⟩-βŠ₯-is-minimum u

    F₁ : F πŸ™
    F₁ f = f ⋆ , (Ξ» ⋆ β†’ ⟨ 𝓑 ⟩-refl (f ⋆)) , Ξ» u ψ β†’ ψ ⋆

    FΟ‰ : ((P : β„• β†’ 𝓣 Μ‡ ) β†’ ((n : β„•) β†’ F (P n)) β†’ F (βˆƒ n κž‰ β„• , P n))
    FΟ‰ P Ο† f = b∞ , α∞ , β∞
     where
      g : (n : β„•) β†’ P n β†’ ⟨ 𝓑 ⟩
      g n p = f ∣ n , p ∣

      h : (n : β„•) β†’ Ξ£ b κž‰ ⟨ 𝓑 ⟩ , (b is-the-join-of g n on 𝓑)
      h n = Ο† n (g n)

      b : β„• β†’ ⟨ 𝓑 ⟩
      b n = pr₁ (h n)

      Ξ± : (n : β„•) (p : P n) β†’ g n p β‰€βŸ¨ 𝓑 ⟩ b n
      Ξ± n = pr₁ (prβ‚‚ (h n))

      Ξ² : (n : β„•) (u : ⟨ 𝓑 ⟩) β†’ ((p : P n) β†’ (g n p) β‰€βŸ¨ 𝓑 ⟩ u) β†’ b n β‰€βŸ¨ 𝓑 ⟩ u
      Ξ² n = prβ‚‚ (prβ‚‚ (h n))

      b∞ : ⟨ 𝓑 ⟩
      b∞ = β‹βŸ¨ 𝓑 ⟩ b

      α∞ : (q : βˆƒ n κž‰ β„• , P n) β†’ f q β‰€βŸ¨ 𝓑 ⟩ b∞
      α∞ = βˆ₯βˆ₯-induction (Ξ» s β†’ ⟨ 𝓑 ⟩-order-is-prop-valued (f s) b∞) α∞'
       where
        α∞' : (Οƒ : Ξ£ n κž‰ β„• , P n) β†’ f ∣ Οƒ ∣ β‰€βŸ¨ 𝓑 ⟩ b∞
        α∞' (n , p) = ⟨ 𝓑 ⟩-trans (g n p) (b n) b∞ (Ξ± n p) (⟨ 𝓑 ⟩-⋁-is-ub b n)

      β∞ : (u : ⟨ 𝓑 ⟩) β†’ ((q : βˆƒ n κž‰ β„• , P n) β†’ f q β‰€βŸ¨ 𝓑 ⟩ u) β†’ b∞ β‰€βŸ¨ 𝓑 ⟩ u
      β∞ u ψ = ⟨ 𝓑 ⟩-⋁-is-lb-of-ubs b u l
       where
        l : (n : β„•) β†’ b n β‰€βŸ¨ 𝓑 ⟩ u
        l n = Ξ² n u (Ξ» p β†’ ψ ∣ n , p ∣)

\end{code}

We repackage the above.

\begin{code}

  module _ {π“₯ 𝓦 : Universe}
           (𝓑 : Οƒ-SupLat π“₯ 𝓦)
           (P : 𝓣 Μ‡ )
           (i : is-quasidecidable P)
           (f : P β†’ ⟨ 𝓑 ⟩)
         where

    sup : ⟨ 𝓑 ⟩
    sup = pr₁ (Οƒ-suplats-have-quasidecidable-joins 𝓑 P i f)

    sup-is-ub : (p : P) β†’ f p β‰€βŸ¨ 𝓑 ⟩ sup
    sup-is-ub = pr₁ (prβ‚‚ (Οƒ-suplats-have-quasidecidable-joins 𝓑 P i f))

    sup-is-lb-of-ubs : (u : ⟨ 𝓑 ⟩) β†’ ((p : P) β†’ f p β‰€βŸ¨ 𝓑 ⟩ u) β†’ sup β‰€βŸ¨ 𝓑 ⟩ u
    sup-is-lb-of-ubs = prβ‚‚ (prβ‚‚ (Οƒ-suplats-have-quasidecidable-joins 𝓑 P i f))

\end{code}

We say that a map is a q-embedding if its fibers are all
quasidecidable. We define three versions of the same definition to
help Agda to solve constraints.

\begin{code}

  is-q-embedding : {X : 𝓣 Μ‡ } {Y : 𝓣 Μ‡ } β†’ (X β†’ Y) β†’ 𝓣 ⁺ Μ‡
  is-q-embedding f = βˆ€ y β†’ is-quasidecidable (fiber f y)

  is-q-embeddingl : {X : 𝓣 Μ‡ } {Y : 𝓀₀ Μ‡ } β†’ (X β†’ Y) β†’ 𝓣 ⁺ Μ‡
  is-q-embeddingl f = βˆ€ y β†’ is-quasidecidable (fiber f y)

  is-q-embeddingr : {X : 𝓀₀ Μ‡ } {Y : 𝓣 Μ‡ } β†’ (X β†’ Y) β†’ 𝓣 ⁺ Μ‡
  is-q-embeddingr f = βˆ€ y β†’ is-quasidecidable (fiber f y)

\end{code}

The following generalizes the existence of quasidecidable-indexed
joins.

\begin{code}

  Οƒ-suplats-have-quasidecidable-joins'
   : (𝓑 : Οƒ-SupLat π“₯ 𝓦) {I : 𝓣 Μ‡ }
   β†’ (f : I β†’ β„•)
   β†’ is-q-embeddingl f
   β†’ (b : β„• β†’ ⟨ 𝓑 ⟩)
   β†’ Ξ£ c κž‰ ⟨ 𝓑 ⟩ , (c is-the-join-of (b ∘ f) on 𝓑)
  Οƒ-suplats-have-quasidecidable-joins' {π“₯} {𝓦} 𝓑 {I} f q b = c , Ξ± , Ξ²
   where
    g : I β†’ ⟨ 𝓑 ⟩
    g = b ∘ f

    a : β„• β†’ A
    a n = pr₁ (q n)

    e : (n : β„•) β†’ Ο„ (a n) holds ＝ (Ξ£ i κž‰ I , f i ＝ n)
    e n = prβ‚‚ (q n)

    Ξ³ : (n : β„•) β†’ Ο„ (a n) holds β†’ (Ξ£ i κž‰ I , f i ＝ n)
    Ξ³ n = Idtofun (e n)

    Ξ΄ : (n : β„•)  β†’ (Ξ£ i κž‰ I , f i ＝ n) β†’ Ο„ (a n) holds
    δ n = Idtofun ((e n)⁻¹)

    g' : (n : β„•) β†’ Ο„ (a n) holds β†’ ⟨ 𝓑 ⟩
    g' n h = g (pr₁ (Ξ³ n h))

    b' : β„• β†’ ⟨ 𝓑 ⟩
    b' n = sup 𝓑 (Ο„ (a n) holds) (a n , refl) (g' n)

    c : ⟨ 𝓑 ⟩
    c = β‹βŸ¨ 𝓑 ⟩ b'

    Ξ± : βˆ€ i β†’ b (f i) β‰€βŸ¨ 𝓑 ⟩ c
    Ξ± i = ⟨ 𝓑 ⟩-trans (b (f i)) (b' (f i)) c lβ‚‚ lβ‚€
     where
      lβ‚€ : b' (f i) β‰€βŸ¨ 𝓑 ⟩ c
      lβ‚€ = ⟨ 𝓑 ⟩-⋁-is-ub b' (f i)

      l₁ : g' (f i) (Ξ΄ (f i) (i , refl)) β‰€βŸ¨ 𝓑 ⟩ b' (f i)
      l₁ = sup-is-ub 𝓑
            (Ο„ (a (f i)) holds)
            (a (f i) , refl)
            (g' (f i))
            (Ξ΄ (f i)
            (i , refl))

      r : g' (f i) (Ξ΄ (f i) (i , refl))
        ＝ b (f (pr₁ (Ξ³ (f i) (Ξ΄ (f i) (i , refl)))))
      r = refl

      s : b (f (pr₁ (Ξ³ (f i) (Ξ΄ (f i) (i , refl))))) ＝ b (f i)
      s = ap (Ξ» - β†’ b (f (pr₁ -))) (Idtofun-retraction (e (f i)) (i , refl))

      t : g' (f i) (δ (f i) (i , refl)) ＝ b (f i)
      t = s

      lβ‚‚ : b (f i) β‰€βŸ¨ 𝓑 ⟩ b' (f i)
      lβ‚‚ = transport (Ξ» - β†’ - β‰€βŸ¨ 𝓑 ⟩ b' (f i)) s l₁

    Ξ² : (u : ⟨ 𝓑 ⟩) β†’ (βˆ€ i β†’ b (f i) β‰€βŸ¨ 𝓑 ⟩ u) β†’ c β‰€βŸ¨ 𝓑 ⟩ u
    Ξ² u Ο† = ⟨ 𝓑 ⟩-⋁-is-lb-of-ubs b' u l
     where
      Ο†' : (n : β„•) (h : Ο„ (a n) holds) β†’ g' n h β‰€βŸ¨ 𝓑 ⟩ u
      Ο†' n h = Ο† (pr₁ (Ξ³ n h))

      l : (n : β„•) β†’ b' n β‰€βŸ¨ 𝓑 ⟩ u
      l n = sup-is-lb-of-ubs 𝓑 (Ο„ (a n) holds) (a n , refl) (g' n) u (Ο†' n)

\end{code}

We now generalize and resize part of the above (without resizing
axioms) by replacing equality by equivalence in the definition of
quasidecidability:

\begin{code}

  is-quasidecidable' : π“₯ Μ‡ β†’ 𝓣 βŠ” π“₯ Μ‡
  is-quasidecidable' P = Ξ£ a κž‰ A , (Ο„ a holds ≃ P)

  is-quasidecidableβ‚€ : 𝓣 Μ‡ β†’ 𝓣 Μ‡
  is-quasidecidableβ‚€ = is-quasidecidable' {𝓣}

  quasidecidability-resizing : (P : 𝓣 Μ‡ )
                             β†’ is-quasidecidable P ≃ is-quasidecidableβ‚€ P
  quasidecidability-resizing P = Ξ£-cong e
   where
    e : (a : A) β†’ (Ο„ a holds ＝ P) ≃ (Ο„ a holds ≃ P)
    e a = prop-univalent-≃' pe fe P (Ο„ a holds) (holds-is-prop (Ο„ a))

  being-quasidecidableβ‚€-is-prop : (P : 𝓣 Μ‡ ) β†’ is-prop (is-quasidecidableβ‚€ P)
  being-quasidecidableβ‚€-is-prop P = equiv-to-prop
                                     (≃-sym (quasidecidability-resizing P))
                                     (being-quasidecidable-is-prop P)

  𝟘-is-quasidecidableβ‚€ : is-quasidecidableβ‚€ 𝟘
  𝟘-is-quasidecidableβ‚€ = ⌜ quasidecidability-resizing 𝟘 ⌝ 𝟘-is-quasidecidable

  πŸ™-is-quasidecidableβ‚€ : is-quasidecidableβ‚€ πŸ™
  πŸ™-is-quasidecidableβ‚€ = ⌜ quasidecidability-resizing πŸ™ ⌝ πŸ™-is-quasidecidable

  quasidecidableβ‚€-closed-under-Ο‰-joins
   : (P : β„• β†’ 𝓣 Μ‡ )
   β†’ ((n : β„•) β†’ is-quasidecidableβ‚€ (P n))
   β†’ is-quasidecidableβ‚€ (βˆƒ n κž‰ β„• , P n)
  quasidecidableβ‚€-closed-under-Ο‰-joins P Ο† =
   ⌜ quasidecidability-resizing (βˆƒ n κž‰ β„• , P n) ⌝
    (quasidecidable-closed-under-Ο‰-joins P Ο†')
   where
    Ο†' : (n : β„•) β†’ is-quasidecidable (P n)
    Ο†' n = ⌜ quasidecidability-resizing (P n) ⌝⁻¹ (Ο† n)

  quasidecidableβ‚€-induction
   : (F : 𝓣 Μ‡ β†’ π“₯ Μ‡ )
   β†’ ((P : 𝓣 Μ‡ ) β†’ is-prop (F P))
   β†’ F 𝟘
   β†’ F πŸ™
   β†’ ((P : β„• β†’ 𝓣 Μ‡ ) β†’ ((n : β„•) β†’ F (P n)) β†’ F (βˆƒ n κž‰ β„• , P n))
   β†’ (P : 𝓣 Μ‡ ) β†’ is-quasidecidableβ‚€ P β†’ F P
  quasidecidableβ‚€-induction F i Fβ‚€ F₁ FΟ‰ P q =
   quasidecidable-induction F i Fβ‚€ F₁ FΟ‰ P (⌜ quasidecidability-resizing P ⌝⁻¹ q)

\end{code}

This concludes the module hypothetical-free-Οƒ-SupLat-on-one-generator.

We now give the proofs of the main theorems by calling the above modules.

\begin{code}

theorem₁ {𝓣} {𝓀} q = free-Οƒ-SupLat-on-one-generator QD ⊀ QD-is-free-Οƒ-SupLat
 where
  open quasidecidable-propositions-exist q
  open hypothetical-quasidecidability {𝓣} {𝓀}
         (quasidecidable-propositions
            is-quasidecidable
            being-quasidecidable-is-prop
            𝟘-is-quasidecidable
            πŸ™-is-quasidecidable
            quasidecidable-closed-under-Ο‰-joins
            quasidecidable-induction)

theoremβ‚‚ {𝓣} {𝓀} f = quasidecidable-propositions
                        is-quasidecidableβ‚€
                        being-quasidecidableβ‚€-is-prop
                        𝟘-is-quasidecidableβ‚€
                        πŸ™-is-quasidecidableβ‚€
                        quasidecidableβ‚€-closed-under-Ο‰-joins
                        quasidecidableβ‚€-induction
 where
  open free-Οƒ-SupLat-on-one-generator-exists f
  open hypothetical-free-Οƒ-SupLat-on-one-generator
  open assumption {𝓣} {𝓀} 𝓐 ⊀ 𝓐-free

theorem₃ {𝓣} {π“š} f = initial-Οƒ-frame 𝓐-qua-Οƒ-frame 𝓐-qua-Οƒ-frame-is-initial
 where
  open free-Οƒ-SupLat-on-one-generator-exists f
  open hypothetical-free-Οƒ-SupLat-on-one-generator
  open assumption {𝓣} {π“š} 𝓐 ⊀ 𝓐-free

theoremβ‚„ {𝓣} {π“š} ρ = quasidecidable-propositions
                        is-quasidecidable
                        being-quasidecidable-is-prop
                        𝟘-is-quasidecidable
                        πŸ™-is-quasidecidable
                        quasidecidable-closed-under-Ο‰-joins
                        quasidecidable-induction
 where
  open quasidecidability-construction-from-resizing 𝓣 π“š ρ

\end{code}

TODO:

  ⋆ Very little here has to do with the nature of the type β„•. We never
    used zero, successor, or induction! (But they are used in another
    module to construct binary joins, which are not used here.) Any
    indexing type replacing β„• works in the above development, with the
    definition of Οƒ-sup-lattice generalized to have an arbitrary (but
    fixed) indexing type in place of β„•. (We could have multiple
    indexing types, but this would require a modification of the above
    development.)

  ⋆ Define, by induction (or as a W-type) a type similar to the
    Brouwer ordinals, with two constructors 0 and 1 and a formal
    β„•-indexed sup operation. We have a unique map to the initial
    Οƒ-sup-lattice that transforms formal sups into sups and maps 0 to
    βŠ₯ and 1 to ⊀. Is this function a surjection (it is definitely not
    an injection), or what (known) axioms are needed for it to be a
    surjection? Countable choice suffices. But is it necessary? It
    seems likely that the choice principle studied in the above paper
    with Cory Knapp is necessary and sufficient. This principle
    implies that the quasidecidable propositions agree with the
    semidecidable ones.