See Ordinals.Arithmetic for the definition of the unique ordinal structure on a
proposition. We prove additional properties here that require several imports.

\begin{code}

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

open import UF.Univalence

module Ordinals.Propositions (ua : Univalence) where

open import UF.FunExt
open import UF.UA-FunExt

private
 fe : FunExt
 fe = Univalence-gives-FunExt ua

 fe' : Fun-Ext
 fe' = Univalence-gives-Fun-Ext ua

open import MLTT.Spartan
open import Ordinals.Arithmetic fe
open import Ordinals.Equivalence
open import Ordinals.OrdinalOfOrdinals ua
open import Ordinals.Type
open import UF.Equiv
open import UF.Subsingletons

prop-ordinal-⊴ : {P : 𝓀 Μ‡  } {Q : π“₯ Μ‡  } (i : is-prop P) (j : is-prop Q)
               β†’ (P β†’ Q) β†’ prop-ordinal P i ⊴ prop-ordinal Q j
prop-ordinal-⊴ _ _ f = f , (Ξ» _ _ β†’ 𝟘-elim) , (Ξ» _ _ β†’ 𝟘-elim)

prop-ordinal-≃ₒ : {P : 𝓀 Μ‡  } {Q : π“₯ Μ‡  } (i : is-prop P) (j : is-prop Q)
                β†’ (P β†’ Q) β†’ (Q β†’ P) β†’ prop-ordinal P i ≃ₒ prop-ordinal Q j
prop-ordinal-≃ₒ {𝓀} {π“₯} {P} {Q} i j f g =
 bisimilarity-gives-ordinal-equiv
  (prop-ordinal P i) (prop-ordinal Q j)
  (prop-ordinal-⊴ i j f)
  (prop-ordinal-⊴ j i g)

prop-ordinal-＝ : {P Q : 𝓀 Μ‡  } (i : is-prop P) (j : is-prop Q)
               β†’ (P β†’ Q) β†’ (Q β†’ P) β†’ prop-ordinal P i ＝ prop-ordinal Q j
prop-ordinal-＝ {𝓀} {P} {Q} i j f g =
 eqtoidβ‚’ (ua 𝓀) fe'
  (prop-ordinal P i) (prop-ordinal Q j) (prop-ordinal-≃ₒ i j f g)

prop-ordinal-↓-≃ₒ : {P : 𝓀 Μ‡  } (i : is-prop P) (p : P)
                  β†’ (prop-ordinal P i ↓ p) ≃ₒ πŸ˜β‚’ {π“₯}
prop-ordinal-↓-≃ₒ {𝓀} {P} i p =
 prop-ordinal-≃ₒ
  (Ξ» (x , l) (y , k) β†’ 𝟘-elim l)
  𝟘-is-prop
  (Ξ» (x , l) β†’ 𝟘-elim l)
  𝟘-elim

prop-ordinal-↓ : {P : 𝓀 Μ‡  } (i : is-prop P) (p : P)
               β†’ (prop-ordinal P i ↓ p) ＝ πŸ˜β‚’
prop-ordinal-↓ i p =
 eqtoidβ‚’ (ua _) fe' (prop-ordinal _ i ↓ p) πŸ˜β‚’ (prop-ordinal-↓-≃ₒ i p)

prop-ordinal-least : {P : 𝓀 Μ‡  } (i : is-prop P) (p : P)
                   β†’ is-least (prop-ordinal P i) p
prop-ordinal-least i p p' p'' l = 𝟘-elim l

πŸ™β‚’-↓ : {x : πŸ™ {𝓀}} β†’ πŸ™β‚’ ↓ x ＝ πŸ˜β‚’
πŸ™β‚’-↓ {𝓀} {x} = prop-ordinal-↓ πŸ™-is-prop x

πŸ™β‚’-↓-≃ₒ : {x : πŸ™ {𝓀}} β†’ (πŸ™β‚’ ↓ x) ≃ₒ πŸ˜β‚’ {π“₯}
πŸ™β‚’-↓-≃ₒ {𝓀} {π“₯} {x} = prop-ordinal-↓-≃ₒ πŸ™-is-prop x

only-one-πŸ™β‚’-⊴ : πŸ™β‚’ {𝓀} ⊴ πŸ™β‚’ {π“₯}
only-one-πŸ™β‚’-⊴ = prop-ordinal-⊴ πŸ™-is-prop πŸ™-is-prop (Ξ» _ β†’ ⋆)

only-one-πŸ™β‚’ : πŸ™β‚’ {𝓀} ≃ₒ πŸ™β‚’ {π“₯}
only-one-πŸ™β‚’ =
 bisimilarity-gives-ordinal-equiv πŸ™β‚’ πŸ™β‚’ only-one-πŸ™β‚’-⊴ only-one-πŸ™β‚’-⊴

only-one-πŸ˜β‚’-⊴ : πŸ˜β‚’ {𝓀} ⊴ πŸ˜β‚’ {π“₯}
only-one-πŸ˜β‚’-⊴ = prop-ordinal-⊴ 𝟘-is-prop 𝟘-is-prop 𝟘-elim

only-one-πŸ˜β‚’ : πŸ˜β‚’ {𝓀} ≃ₒ πŸ˜β‚’ {π“₯}
only-one-πŸ˜β‚’ =
 bisimilarity-gives-ordinal-equiv πŸ˜β‚’ πŸ˜β‚’ only-one-πŸ˜β‚’-⊴ only-one-πŸ˜β‚’-⊴

πŸ™β‚’-⊴-shift : (Ξ± : Ordinal 𝓦) β†’ πŸ™β‚’ {𝓀} ⊴ Ξ± β†’ πŸ™β‚’ {π“₯} ⊴ Ξ±
πŸ™β‚’-⊴-shift Ξ± = ⊴-trans πŸ™β‚’ πŸ™β‚’ Ξ± only-one-πŸ™β‚’-⊴

πŸ˜β‚’-⊲⁻-πŸ™β‚’ : πŸ˜β‚’ {𝓀} ⊲⁻ πŸ™β‚’ {π“₯}
πŸ˜β‚’-⊲⁻-πŸ™β‚’ = ⋆ , ≃ₒ-sym (πŸ™β‚’ ↓ ⋆) πŸ˜β‚’ (prop-ordinal-↓-≃ₒ πŸ™-is-prop ⋆)

πŸ˜β‚’-⊲-πŸ™β‚’ : πŸ˜β‚’ {𝓀} ⊲ πŸ™β‚’ {𝓀}
πŸ˜β‚’-⊲-πŸ™β‚’ = ⌜ ⊲-is-equivalent-to-⊲⁻ πŸ˜β‚’ πŸ™β‚’ ⌝⁻¹ πŸ˜β‚’-⊲⁻-πŸ™β‚’

holds-gives-equal-πŸ™β‚’ : {P : 𝓀 Μ‡  } (i : is-prop P) β†’ P β†’ prop-ordinal P i ＝ πŸ™β‚’
holds-gives-equal-πŸ™β‚’ i p = prop-ordinal-＝ i πŸ™-is-prop (Ξ» _ β†’ ⋆) (Ξ» _ β†’ p)

\end{code}