Tom de Jong and Martin Escardo
January 2026

This file follows the definitions, equations, lemmas, propositions, theorems and
remarks of our paper

   Tom de Jong and MartΓ­n HΓΆtzel EscardΓ³
   Examples and counterexamples of injective types
   January 2026
   https://arxiv.org/abs/TODO

\begin{code}

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

\end{code}

Our global assumptions are univalence and the existence of propositional
truncations.

Function extensionality and propositional extensionality can be derived from
univalence.

\begin{code}

open import UF.Univalence
open import UF.PropTrunc

module InjectiveTypes.ExamplesCounterExamplesArticle
       (ua : Univalence)
       (pt : propositional-truncations-exist)
       where

open import MLTT.Spartan

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

open PropositionalTruncation pt

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

 fe' : Fun-Ext
 fe' {𝓀} {π“₯} = fe 𝓀 π“₯

 pe : PropExt
 pe = Univalence-gives-PropExt ua

 pe' : Prop-Ext
 pe' {𝓀} = pe 𝓀

open import Apartness.Definition
open import Apartness.Properties pt
open Apartness pt

open import UF.Choice
open world's-simplest-axiom-of-choice fe pt
open import CoNaturals.Type
open import DedekindReals.Type fe' pe' pt
open import DedekindReals.Order fe' pe' pt renaming (_β™―_ to _♯ℝ_)

open import Notation.CanonicalMap
open import Notation.General
open import Notation.Order

open import InjectiveTypes.Blackboard fe hiding (extension)
open import InjectiveTypes.CharacterizationViaLifting fe
open import InjectiveTypes.CounterExamples ua pt
open import InjectiveTypes.InhabitedTypesTaboo pt ua
open import InjectiveTypes.NonEmptyTypes pt ua
open import InjectiveTypes.OverSmallMaps fe
open import InjectiveTypes.PointedDcpos fe pt
open import InjectiveTypes.Resizing ua pt
open import InjectiveTypes.Subtypes fe

open import Iterative.Multisets
open import Iterative.Multisets-Addendum ua
open import Iterative.Sets ua
open import Iterative.Sets-Addendum ua

open import Ordinals.Injectivity
open import Ordinals.Type

open import Quotient.Type

open import SyntheticHomotopyTheory.RP-infinity pt

open import Taboos.BasicDiscontinuity fe'
open import Taboos.Decomposability fe
open decomposability pt
open decomposability-bis pt
open import Taboos.WLPO
open import TypeTopology.SimpleTypes fe pt
open import TypeTopology.TotallySeparated

open import UF.Base
open import UF.ClassicalLogic
open import UF.Embeddings
open import UF.Equiv
open import UF.ExitPropTrunc
open split-support-and-collapsibility pt
open import UF.NotNotStablePropositions
open import UF.PropIndexedPiSigma
open import UF.Retracts
open import UF.SIP-Examples
open import UF.Size
open import UF.Subsingletons-FunExt
open import UF.SubtypeClassifier

open import Various.DedekindNonAxiomatic pt fe' pe' using (π“‘βˆž)

\end{code}

Section 2. Preliminaries

\begin{code}

Definition-2-1 : (𝓀 : Universe) β†’ 𝓀 ⁺ Μ‡
Definition-2-1 𝓀 = is-small (ꪪ 𝓀)

Lemma-2-2 : {X : 𝓀 Μ‡} (A : X β†’ π“₯ Μ‡) (B : (x : X) β†’ A x β†’ 𝓦 Μ‡ )
            (x y : X) (a : A x) (b : B x a) (p : x ＝ y)
          β†’ transport (Ξ» - β†’ Sigma (A -) (B -)) p (a , b)
            ＝ transport A p a , transportd A B a p b
Lemma-2-2 A B x y a b p = transport-Ξ£ A B y p a {b}

module _
        {X : 𝓀 Μ‡ } (a : X) {Y : X β†’ π“₯ Μ‡ } (i : is-prop X)
       where

 Lemma-2-3-i : Ξ  Y ≃ Y a
 Lemma-2-3-i = prop-indexed-product a fe' i

 Lemma-2-3-i₁ : ⌜ Lemma-2-3-i ⌝ ＝ (Ξ» f β†’ f a)
 Lemma-2-3-i₁ = refl

 Lemma-2-3-iβ‚‚ : ⌜ Lemma-2-3-i ⌝⁻¹ ＝ (Ξ» y x β†’ transport Y (i a x) y)
 Lemma-2-3-iβ‚‚ = refl

 Lemma-2-3-ii : Y a ≃ Ξ£ Y
 Lemma-2-3-ii = ≃-sym (prop-indexed-sum a i)

 Lemma-2-3-ii₁ : ⌜ Lemma-2-3-ii ⌝ ＝ (Ξ» y β†’ (a , y))
 Lemma-2-3-ii₁ = refl

 Lemma-2-3-iiβ‚‚ : ⌜ Lemma-2-3-ii ⌝⁻¹ ＝ (Ξ» (x , y) β†’ transport Y (i x a) y)
 Lemma-2-3-iiβ‚‚ = refl

\end{code}

Section 3. Flabbiness and injectivity

\begin{code}

Definition-3-1 : (D : 𝓦 Μ‡ ) (𝓀 π“₯ : Universe) β†’ (𝓀 βŠ” π“₯) ⁺ βŠ” 𝓦 Μ‡
Definition-3-1 = ainjective-type

Definition-3-2 : (D : 𝓦 Μ‡ ) (𝓀 : Universe) β†’ 𝓀 ⁺ βŠ” 𝓦 Μ‡
Definition-3-2 = aflabby

Lemma-3-3-i : (D : 𝓦 Μ‡ ) β†’ ainjective-type D 𝓀 π“₯ β†’ aflabby D 𝓀
Lemma-3-3-i = ainjective-types-are-aflabby

Lemma-3-3-ii : (D : 𝓦 Μ‡ ) β†’ aflabby D (𝓀 βŠ” π“₯) β†’ ainjective-type D 𝓀 π“₯
Lemma-3-3-ii = aflabby-types-are-ainjective

Lemma-3-4 : (D : 𝓦 Μ‡ ) β†’ ainjective-type D 𝓀 π“₯
          β†’ (D' : 𝓦 Μ‡ ) β†’ retract D' of D β†’ ainjective-type D' 𝓀 π“₯
Lemma-3-4 D ainj D' = retract-of-ainjective D' D ainj

Lemma-3-5 : (D : 𝓦 Μ‡ ) β†’ aflabby D 𝓣
          β†’ (X : 𝓀 Μ‡ ) (Y : π“₯ Μ‡ ) (j : X β†’ Y)
          β†’ is-embedding j
          β†’ j is 𝓣 small-map
          β†’ (f : X β†’ D)
          β†’ Ξ£ f' κž‰ (Y β†’ D) , f' ∘ j ∼ f
Lemma-3-5 D aflab X Y = aflabbiness-gives-injectivity-over-small-maps D aflab

Lemma-3-6 : {𝓦 𝓀 π“₯ 𝓣₀ 𝓣₁ 𝓣₂ : Universe}
          β†’ (D : 𝓦 Μ‡ ) β†’ ainjective-type D (𝓣₀ βŠ” 𝓣₁) 𝓣₂
          β†’ (X : 𝓀 Μ‡ ) (Y : π“₯ Μ‡ ) (j : X β†’ Y)
          β†’ is-embedding j
          β†’ j is 𝓣₀ small-map
          β†’ (f : X β†’ D)
          β†’ Ξ£ f' κž‰ (Y β†’ D) , f' ∘ j ∼ f
Lemma-3-6 {𝓦} {𝓀} {π“₯} {𝓣₀} {𝓣₁} {𝓣₂} D ainj X Y j =
 ainjectivity-over-small-maps 𝓣₁ D ainj j

module _
        {𝓀 π“₯ 𝓣₀ 𝓣₁ 𝓣₂ : Universe}
        (D : 𝓀 Μ‡ ) (ainj : ainjective-type D (𝓣₀ βŠ” 𝓣₁) 𝓣₂)
        (Y : π“₯ Μ‡ ) (j : D β†’ Y)
        (j-emb : is-embedding j)
        (j-small : j is 𝓣₀ small-map)
       where

 Lemma-3-7-i : retract D of Y
 Lemma-3-7-i = embedding-retract' 𝓣₁ D Y j j-emb j-small ainj

 Lemma-3-7-ii : section Lemma-3-7-i ＝ j
 Lemma-3-7-ii = refl

module _
        (𝓣 : Universe)
       where

 open ainjectivity-of-Lifting 𝓣
 open ainjectivity-of-Lifting' 𝓣 (ua 𝓣)

 Lemma-3-8 : (X : 𝓀 Μ‡ ) β†’ (Ξ· ∢ (X β†’ 𝓛 X)) is 𝓣 small-map
 Lemma-3-8 X = Ξ·-is-small-map

 Lemma-3-9 : (D : 𝓀 Μ‡ ) β†’ ainjective-type D (π“₯ βŠ” 𝓣) 𝓦
           β†’ retract D of 𝓛 D
 Lemma-3-9 {𝓀} {π“₯} = ainjective-is-retract-of-free-𝓛-algebra' π“₯

 Theorem-3-10 : (D : 𝓀 Μ‡ )
              β†’ ainjective-type D 𝓣 𝓣 ↔ (Ξ£ X κž‰ 𝓀 Μ‡  , retract D of 𝓛 X)
 Theorem-3-10 = ainjectives-in-terms-of-free-𝓛-algebras'

 Theorem-3-11
  : (D : 𝓀 Μ‡ )
  β†’ ainjective-type D 𝓣 𝓣 ↔ (Ξ£ A κž‰ 𝓣 ⁺ βŠ” 𝓀 Μ‡  , 𝓛-alg A Γ— (retract D of A))
 Theorem-3-11 = ainjectives-in-terms-of-𝓛-algebras

\end{code}

Section 4. Examples

\begin{code}

Examples-1-i : ainjective-type (𝓀 Μ‡ ) 𝓀 𝓀
Examples-1-i {𝓀} = universes-are-ainjective-Ξ£ (ua 𝓀)

Examples-1-ii : ainjective-type (𝓀 Μ‡ ) 𝓀 𝓀
Examples-1-ii {𝓀} = universes-are-ainjective-Ξ  (ua 𝓀)

Examples-2 : ainjective-type (Ξ© 𝓀) 𝓀 𝓀
Examples-2 {𝓀} = Ξ©-ainjective pe'

\end{code}

Examples (3)β€”(5) can be found below and are postponed for now (as in the paper).

\begin{code}

Examples-6-i : set-quotients-exist β†’ ainjective-type (Ordinal 𝓀) 𝓀 𝓀
Examples-6-i {𝓀} sqe =
 pointed-dcpos-are-ainjective-types 𝓀 (Ord-DCPO , πŸ˜β‚’ , πŸ˜β‚’-least-⊴)
  where
   open import DomainTheory.Basics.Dcpo pt fe' 𝓀
   open import Ordinals.AdditionProperties ua
   open import Ordinals.Arithmetic fe
   open import Ordinals.Equivalence
   open import Ordinals.OrdinalOfOrdinals ua
   open import Ordinals.OrdinalOfOrdinalsSuprema ua
   open import Quotient.GivesSetReplacement

   sr : Set-Replacement pt
   sr = set-replacement-from-set-quotients-and-prop-trunc sqe pt

   Ord-DCPO : DCPO {𝓀 ⁺} {𝓀}
   Ord-DCPO = (Ordinal 𝓀 , _⊴_ ,
               (the-type-of-ordinals-is-a-set (ua 𝓀) fe' ,
                ⊴-is-prop-valued , ⊴-refl , ⊴-trans , ⊴-antisym) ,
               (Ξ» I Ξ± _ β†’ ordinal-of-ordinals-has-small-suprema' pt sr I Ξ±))
    where
     open suprema pt sr

Examples-6-ii : ainjective-type (Ordinal 𝓀) 𝓀 𝓀
Examples-6-ii {𝓀} = Ordinal-is-ainjective (ua 𝓀)
 where
  open ordinals-injectivity fe

Proposition-4-1 : let NE = (Ξ£ X κž‰ 𝓀 Μ‡  , ¬¬ X) in
                  (retract NE of (𝓀 Μ‡ )) Γ— ainjective-type NE 𝓀 𝓀
Proposition-4-1 {𝓀} = Non-Empty-retract 𝓀 , Non-Empty-is-injective 𝓀

Lemma-4-2 : (P : 𝓣 Μ‡ ) (X : P β†’ 𝓀 Μ‡ ) β†’ is-prop P
          β†’ (Ξ  p κž‰ P , ¬¬ X p) β†’ ¬¬ Ξ  X
Lemma-4-2 P X i Ο† Ξ½ = Ξ½ III
 where
  I : (p : P) β†’ Β¬ X p
  I p x = Ξ½ (Ξ» p' β†’ transport X (i p p') x)
  II : Β¬ P
  II p = Ο† p (I p)
  III : (p : P) β†’ X p
  III p = 𝟘-elim (II p)

Proposition-4-1-alt : ainjective-type (Ξ£ X κž‰ 𝓀 Μ‡  , ¬¬ X) 𝓀 𝓀
Proposition-4-1-alt =
 ainjectivity-of-type-of-structures (¬¬_) (Π-closure-criterion ¬¬_ T T-refl c)
  where
   open import InjectiveTypes.MathematicalStructures ua
   T : {X Y : 𝓀 Μ‡ } β†’ (X ≃ Y) β†’ ¬¬ X β†’ ¬¬ Y
   T 𝕗 = ¬¬-functor ⌜ 𝕗 ⌝
   T-refl : {X : 𝓀 Μ‡ } β†’ T (≃-refl X) ∼ id
   T-refl x = refl
   c : closed-under-prop-Π' ¬¬_ T T-refl
   c (P , i) X = m-is-equiv
    where
     m : ¬¬ Ξ  X β†’ Ξ  p κž‰ P , ¬¬ X p
     m h p = T (prop-indexed-product p fe' i) h
     m-is-equiv : is-equiv m
     m-is-equiv = qinvs-are-equivs m
                   (Lemma-4-2 P X i ,
                    (Ξ» _ β†’ negations-are-props fe' _ _) ,
                    (Ξ» _ β†’ Ξ -is-prop fe' (Ξ» p β†’ negations-are-props fe') _ _))

module _
        (π“₯ : Universe)
       where

 open import DomainTheory.Basics.Pointed pt fe' π“₯

 Proposition-4-3 : (𝓓 : DCPOβŠ₯ {𝓀} {𝓣}) β†’ ainjective-type βŸͺ 𝓓 ⟫ π“₯ π“₯
 Proposition-4-3 = pointed-dcpos-are-ainjective-types π“₯

Example-4-4 : ainjective-type π“‘βˆž 𝓀₀ 𝓀₀
Example-4-4 = pointed-dcpos-are-ainjective-types 𝓀₀ π“‘βˆž-DCPOβŠ₯
 where
  open import DomainTheory.Examples.ExtendedPartialDedekindReals pt fe' pe'

Theorem-4-5 : aflabby (𝕄 𝓀) 𝓀
Theorem-4-5 {𝓀} = 𝕄-is-aflabby-Ξ£ 𝓀

Corollary-4-6 : ainjective-type (𝕄 𝓀) 𝓀 𝓀
Corollary-4-6 {𝓀} = 𝕄-is-ainjective-Ξ£ 𝓀

Theorem-4-7 : set-quotients-exist β†’ ainjective-type (𝕍 𝓀) 𝓀 𝓀
Theorem-4-7 {𝓀} sqe = 𝕍-is-ainjective 𝓀 pt sr
 where
  open import Quotient.GivesSetReplacement
  sr : Set-Replacement pt
  sr = set-replacement-from-set-quotients-and-prop-trunc sqe pt

module _
        (S : 𝓀 Μ‡  β†’ π“₯ Μ‡ )
       where

 open import InjectiveTypes.MathematicalStructures ua

 Definition-4-8 : 𝓀 ⁺ βŠ” π“₯ Μ‡
 Definition-4-8 = closed-under-prop-Ξ  S

 Lemma-4-9 : closed-under-prop-Ξ  S β†’ aflabby (Ξ£ S) 𝓀
 Lemma-4-9 = aflabbiness-of-type-of-structured-types S

 module _
         (T : {X Y : 𝓀 Μ‡ } β†’ X ≃ Y β†’ S X β†’ S Y)
         (r : {X : 𝓀 Μ‡ } β†’ T (≃-refl X) ∼ id)
        where

  open canonical-map' S T r

  Lemma-4-10-i : {X Y : 𝓀 Μ‡ } (h : X ≃ Y)
               β†’ T h ∼ treq S h
  Lemma-4-10-i = transport-eqtoid S T r

  Lemma-4-10-ii
   : (P : Ξ© 𝓀) (A : P holds β†’ 𝓀 Μ‡ ) (s : S (Ξ  A)) (p : P holds)
   β†’ ρ P A s p ＝ T (Ο€ P A p) s
  Lemma-4-10-ii P A s p = happly (ρ-and-Ο„-agree P A s) p

module _
       where

 open import InjectiveTypes.MathematicalStructures ua

 Lemma-4-11 : {𝓀 π“₯₁ π“₯β‚‚ : Universe} (S₁ : 𝓀 Μ‡ β†’ π“₯₁ Μ‡ ) (Sβ‚‚ : 𝓀 Μ‡  β†’ π“₯β‚‚ Μ‡ )
            β†’ closed-under-prop-Ξ  S₁
            β†’ closed-under-prop-Ξ  Sβ‚‚
            β†’ closed-under-prop-Ξ  (Ξ» X β†’ S₁ X Γ— Sβ‚‚ X)
 Lemma-4-11 S₁ Sβ‚‚ = closure-under-prop-Ξ -Γ—

 Lemma-4-12 : (S : 𝓀 Μ‡ β†’ π“₯ Μ‡) (S-closed : closed-under-prop-Ξ  S)
              (π”ž : (X : 𝓀 Μ‡) β†’ S X β†’ Ξ© 𝓦)
            β†’ ((P : Ξ© 𝓀) (A : P holds β†’ 𝓀 Μ‡)
               β†’ (Ξ± : (p : P holds) β†’ S (A p))
               β†’ ((p : P holds) β†’ π”ž (A p) (Ξ± p) holds)
               β†’ π”ž (Ξ  A) (inverse (canonical-map.ρ S P A) (S-closed P A) Ξ±) holds)
            β†’ closed-under-prop-Ξ  (Ξ» X β†’ Ξ£ s κž‰ S X , π”ž X s holds)
 Lemma-4-12 S S-closed π”ž =
  closure-under-prop-Ξ -with-axioms S S-closed
   (Ξ» X s β†’ π”ž X s holds) (Ξ» X s β†’ holds-is-prop (π”ž X s))

module Examples-4-13-a where
 open import InjectiveTypes.MathematicalStructures ua

 [1] : ainjective-type (Pointed-type 𝓀) 𝓀 𝓀
 [1] = ainjectivity-of-type-of-pointed-types

 [2] : ainjective-type (∞-Magma 𝓀) 𝓀 𝓀
 [2] = ainjectivity-of-∞-Magma

 [3] : ainjective-type (∞-Magma 𝓀) 𝓀 𝓀
 [3] = ainjectivity-of-∞-Magma

 [4] : ainjective-type (monoid.Monoid {𝓀}) 𝓀 𝓀
 [4] = ainjectivity-of-Monoid

 [5] : ainjective-type (group.Group {𝓀}) 𝓀 𝓀
 [5] = ainjectivity-of-Group

module Examples-4-13-b where
 open import InjectiveTypes.MathematicalStructuresMoreGeneral ua

 [6] : ainjective-type (Graph 𝓀) 𝓀 𝓀
 [6] = ainjectivity-of-Graph

 [7] : ainjective-type (Poset 𝓀) 𝓀 𝓀
 [7] = ainjectivity-of-Poset

 [8] : ainjective-type (Fam 𝓀) 𝓀 𝓀
 [8] = ainjectivity-of-Fam

 [9] : ainjective-type (Ξ£ X κž‰ 𝓀 Μ‡  , Ξ£ Y κž‰ 𝓀 Μ‡  , (X β†’ Y)) 𝓀 𝓀
 [9] = ainjectivity-of-type-of-all-functions

module _
        (X : 𝓀 Μ‡ )
        (A : X β†’ π“₯ Μ‡ )
        (Ο• : aflabby X 𝓦)
        where
 open import InjectiveTypes.Sigma fe

 Definition-4-14 : (P : Ξ© 𝓦) (f : P holds β†’ X)
                 β†’ A (extension Ο• P f) β†’ Ξ  p κž‰ P holds , A (f p)
 Definition-4-14 = ρ A Ο•

 Theorem-4-15 : compatibility-data A Ο• β†’ aflabby (Ξ£ x κž‰ X , A x) 𝓦
 Theorem-4-15 = Ξ£-is-aflabby A Ο•

 Corollary-4-16 : ((x : X) β†’ is-prop (A x))
                β†’ ((P : Ξ© 𝓦) (f : P holds β†’ X)
                      β†’ (Ξ  p κž‰ P holds , A (f p)) β†’ A (extension Ο• P f))
                β†’ aflabby (Ξ£ x κž‰ X , A x) 𝓦
 Corollary-4-16 = subtype-is-aflabby A Ο•

 Proposition-4-17
  : {𝓀 : Universe}
  β†’ Ξ£ X κž‰ 𝓀 ⁺ Μ‡
    , Ξ£ A κž‰ (X β†’ 𝓀 Μ‡ ) , ainjective-type (Ξ£ x κž‰ X , A x) 𝓀 𝓀
                      Γ— (ainjective-type X 𝓀 𝓀 β†’ Propositions-Are-Projective 𝓀)
 Proposition-4-17 {𝓀} =
  example-of-injective-sum-whose-index-type-may-not-be-injective 𝓀

module _ where
 open import InjectiveTypes.Sigma fe

 Lemma-4-18-i : {𝓀 π“₯₁ π“₯β‚‚ 𝓦 : Universe} {X : 𝓀 Μ‡} (Ο• : aflabby X 𝓦)
                {A₁ : X β†’ π“₯₁ Μ‡} {Aβ‚‚ : X β†’ π“₯β‚‚ Μ‡}
              β†’ compatibility-data A₁ Ο•
              β†’ compatibility-data Aβ‚‚ Ο•
              β†’ compatibility-data (Ξ» x β†’ A₁ x Γ— Aβ‚‚ x) Ο•
 Lemma-4-18-i = compatibility-data-Γ—

 Lemma-4-18-ii : {𝓀 π“₯₁ π“₯β‚‚ 𝓦 : Universe} {X : 𝓀 Μ‡} (Ο• : aflabby X 𝓦)
                 {A₁ : X β†’ π“₯₁ Μ‡} {Aβ‚‚ : X β†’ π“₯β‚‚ Μ‡}
               β†’ compatibility-condition A₁ Ο•
               β†’ compatibility-condition Aβ‚‚ Ο•
               β†’ compatibility-condition (Ξ» x β†’ A₁ x Γ— Aβ‚‚ x) Ο•
 Lemma-4-18-ii = compatibility-condition-Γ—

 Lemma-4-19-i
  : {X : 𝓀 Μ‡ } (Ο• : aflabby X π“₯) (A : X β†’ 𝓦 Μ‡ )
    (ρ-has-section : compatibility-data A Ο•)
    (B : (x : X ) β†’ A x β†’ π“₯ Μ‡ )
    (B-is-prop-valued : (x : X) (a : A x) β†’ is-prop (B x a))
    (B-is-closed-under-extension
      : (p : Ξ© π“₯ )
        (f : p holds β†’ X)
      β†’ (Ξ± : (h : p holds) β†’ A (f h))
      β†’ ((h : p holds) β†’ B (f h) (Ξ± h))
      β†’ B (extension Ο• p f) (section-map (ρ A Ο• p f) (ρ-has-section p f) Ξ±))
  β†’ compatibility-data (Ξ» x β†’ Ξ£ a κž‰ A x , B x a) Ο•
 Lemma-4-19-i = compatibility-data-with-axioms

 Lemma-4-19-ii
  : {X : 𝓀 Μ‡ } (Ο• : aflabby X π“₯) (A : X β†’ 𝓦 Μ‡ )
    (ρ-is-equiv : compatibility-condition A Ο•)
    (B : (x : X ) β†’ A x β†’ π“₯ Μ‡ )
    (B-is-prop-valued : (x : X) (a : A x) β†’ is-prop (B x a))
    (B-is-closed-under-extension
      : (p : Ξ© π“₯ )
        (f : p holds β†’ X)
      β†’ (Ξ± : (h : p holds) β†’ A (f h))
      β†’ ((h : p holds) β†’ B (f h) (Ξ± h))
      β†’ B (extension Ο• p f) (inverse (ρ A Ο• p f) (ρ-is-equiv p f) Ξ±))
  β†’ compatibility-condition (Ξ» x β†’ Ξ£ a κž‰ A x , B x a) Ο•
 Lemma-4-19-ii = compatibility-condition-with-axioms

module _
         (S : 𝓀 Μ‡  β†’ π“₯ Μ‡ )
         (T : {X Y : 𝓀 Μ‡ } β†’ X ≃ Y β†’ S X β†’ S Y)
         (r : {X : 𝓀 Μ‡ } β†’ T (≃-refl X) ∼ id)
       where
 open import InjectiveTypes.MathematicalStructuresMoreGeneral ua
 open import InjectiveTypes.Sigma fe using (compatibility-data)
 open import MetricSpaces.StandardDefinition fe' pe' pt

 Definition-4-20-i : (P : Ξ© 𝓀) (A : P holds β†’ 𝓀 Μ‡)
                   β†’ S (Ξ£ A) β†’ Ξ  p κž‰ P holds , S (A p)
 Definition-4-20-i = ρΣ S T r

 Definition-4-20-ii : (P : Ξ© 𝓀) (A : P holds β†’ 𝓀 Μ‡)
                      (s : S (Ξ£ A)) (p : P holds)
                    β†’ Definition-4-20-i P A s p ＝ T (≃-sym (Ξ£-π•šπ•Ÿ P p)) s
 Definition-4-20-ii P A s p = refl

 Definition-4-21 : 𝓀 ⁺ βŠ” π“₯ Μ‡
 Definition-4-21 = compatibility-data-Ξ£ S T r

 Lemma-4-22 : compatibility-data-Ξ£ S T r
            β†’ compatibility-data S universes-are-flabby-Ξ£
 Lemma-4-22 = Ξ£-construction S T r

 Theorem-4-23 : compatibility-data-Ξ£ S T r
              β†’ aflabby (Ξ£ X κž‰ 𝓀 Μ‡  , S X) 𝓀
 Theorem-4-23 comp =
  Theorem-4-15 (𝓀 Μ‡ ) S universes-are-flabby-Ξ£ (Lemma-4-22 comp)

 Example-4-24-1 : (R : π“₯ Μ‡ ) β†’ ainjective-type (Graph' R 𝓀) 𝓀 𝓀
 Example-4-24-1 R = ainjectivity-of-Graph' R

 Example-4-24-2 : {𝓀 : Universe} β†’ let π“₯ = 𝓀₁ βŠ” 𝓀 in
                  ainjective-type (Metric-Space π“₯) π“₯ π“₯
 Example-4-24-2 {𝓀} = ainjectivity-of-Metric-Space pt {𝓀}

Lemma-4-25 : (D : 𝓀 Μ‡ ) (P : D β†’ π“₯ Μ‡ ) β†’ ((d : D) β†’ is-prop (P d))
           β†’ has-retraction (pr₁ ∢ ((Ξ£ d κž‰ D , P d) β†’ D))
           ↔ (Ξ£ f κž‰ (D β†’ D) , ((d : D) β†’ P (f d)) Γ— ((d : D) β†’ P d β†’ f d ＝ d))
Lemma-4-25 = canonical-embedding-has-retraction-reformulation

Theorem-4-26
 : (𝓀 π“₯ 𝓦 𝓣 : Universe)
 β†’ (D : 𝓀 Μ‡ ) β†’ ainjective-type D (π“₯ βŠ” 𝓦) 𝓣
 β†’ (P : D β†’ π“₯ Μ‡ ) β†’ ((d : D) β†’ is-prop (P d))
 β†’ (ainjective-type (Ξ£ P) (π“₯ βŠ” 𝓦) 𝓣 ↔ retract (Ξ£ P) of D)
 Γ— (retract (Ξ£ P) of D ↔ has-retraction (pr₁ ∢ (Ξ£ P β†’ D)))
 Γ— (has-retraction (pr₁ ∢ (Ξ£ P β†’ D))
   ↔ (Ξ£ f κž‰ (D β†’ D) , ((d : D) β†’ P (f d)) Γ— ((d : D) β†’ P d β†’ f d ＝ d)))
Theorem-4-26 𝓀 π“₯ 𝓦 𝓣 D D-ainj P P-prop =
 ([3]β‡’[2] ∘ [1]β‡’[3] , [2]β‡’[1]) ,
 ([1]β‡’[3] ∘ [2]β‡’[1] , [3]β‡’[2]) ,
 [3]⇔[4]
  where
   [1]β‡’[3] : ainjective-type (Ξ£ P) (π“₯ βŠ” 𝓦) 𝓣 β†’ has-retraction (pr₁ ∢ (Ξ£ P β†’ D))
   [1]β‡’[3] =
    canonical-embedding-has-retraction-if-subtype-is-ainjective D P P-prop {𝓦}
   [3]β‡’[2] : has-retraction (pr₁ ∢ (Ξ£ P β†’ D)) β†’ retract (Ξ£ P) of D
   [3]β‡’[2] (s , ρ) = (s , pr₁ , ρ)
   [3]⇔[4] : has-retraction (-id (Sigma D P β†’ D) (Ξ» r β†’ pr₁ r))
           ↔ (Ξ£ f κž‰ (D β†’ D) , ((d : D) β†’ P (f d)) Γ— ((d : D) β†’ P d β†’ f d ＝ d))
   [3]⇔[4] = Lemma-4-25 D P P-prop
   [2]β‡’[1] : retract (Ξ£ P) of D β†’ ainjective-type (Ξ£ P) (π“₯ βŠ” 𝓦) 𝓣
   [2]β‡’[1] = ainjective-subtype-if-retract D P P-prop D-ainj

Lemma-4-27 : (D : 𝓀 Μ‡ ) β†’ ainjective-type D 𝓦 𝓣
           β†’ (P : D β†’ π“₯ Μ‡ ) β†’ ((d : D) β†’ is-prop (P d))
           β†’ retract (Ξ£ P) of D β†’ ainjective-type (Ξ£ P) 𝓦 𝓣
Lemma-4-27 D D-ainj P P-prop = ainjective-subtype-if-retract D P P-prop D-ainj

Corollary-4-28 : (D : 𝓀 ⁺ Μ‡ ) β†’ ainjective-type D 𝓀 𝓀
               β†’ (P : D β†’ 𝓀 Μ‡ ) β†’ ((d : D) β†’ is-prop (P d))
               β†’ ainjective-type (Ξ£ d κž‰ D , P d) 𝓀 𝓀
               ↔ retract (Ξ£ P) of D
Corollary-4-28 {𝓀} D D-ainj P P-prop =
 pr₁ (Theorem-4-26 (𝓀 ⁺) 𝓀 𝓀 𝓀 D D-ainj P P-prop)

module _ where
 open import Modal.Subuniverse

 Corollary-4-29 : (P : subuniverse 𝓀 π“₯) β†’ subuniverse-is-reflective P
                β†’ ainjective-type (subuniverse-member P) 𝓀 𝓀
 Corollary-4-29 {𝓀} {π“₯} β„™@(P , P-prop) P-reflective =
  sufficient-condition-for-injectivity-of-subtype
   (𝓀 Μ‡ ) P P-prop (universes-are-ainjective-Ξ ' (ua 𝓀))
   (β—‹ , β—‹-is-modal , I)
  where
   open import Modal.ReflectiveSubuniverse β„™ P-reflective
   I : (A : 𝓀 Μ‡) β†’ P A β†’ β—‹ A ＝ A
   I A A-modal = eqtoid (ua 𝓀) (β—‹ A) A
                  (≃-sym (Ξ· A , is-modal-gives-Ξ·-is-equiv fe' A A-modal))

\end{code}

Section 4.7. Β΄Models of generalized algebraic theoriesΒ΄ is not formalized.
This concludes Section 4.

Section 5. Weak excluded middle and De Morgan's Law

\begin{code}

Lemma-5-1 : (A : 𝓀 Μ‡ ) (B : π“₯ Μ‡ )
          β†’ is-prop (A + B) ↔ is-prop A Γ— is-prop B Γ— Β¬ (A Γ— B)
Lemma-5-1 A B =
 (Ξ» k β†’ pr₁ (I k) , pr₁ (prβ‚‚ (I k)) , Ξ» (a , b) β†’ prβ‚‚ (prβ‚‚ (I k)) a b) ,
 (Ξ» (i , j , Ξ½) β†’ +-is-prop i j (Ξ» a b β†’ Ξ½ (a , b)))
  where
   I : is-prop (A + B) β†’ is-prop A Γ— is-prop B Γ— (A β†’ B β†’ 𝟘)
   I = sum-of-contradictory-props'-converse

Theorem-5-2-i
 : (WEM 𝓀 ↔ typal-WEM 𝓀)
 Γ— (typal-WEM 𝓀 ↔ De-Morgan pt 𝓀)
 Γ— (De-Morgan pt 𝓀 ↔ typal-De-Morgan pt 𝓀)
 Γ— (typal-De-Morgan pt 𝓀 ↔ untruncated-De-Morgan 𝓀)
 Γ— (untruncated-De-Morgan 𝓀 ↔ untruncated-typal-De-Morgan 𝓀)
Theorem-5-2-i {𝓀} =
 ([1]β‡’[2] , [3]β‡’[1] ∘ [5]β‡’[3] ∘ [6]β‡’[5] ∘ [2]β‡’[6]) ,
 ([5]β‡’[3] ∘ [6]β‡’[5] ∘ [2]β‡’[6] , [1]β‡’[2] ∘ [3]β‡’[1]) ,
 ([6]β‡’[4] ∘ [2]β‡’[6] ∘ [1]β‡’[2] ∘ [3]β‡’[1] , [4]β‡’[3]) ,
 ([6]β‡’[5] ∘ [2]β‡’[6] ∘ [1]β‡’[2] ∘ [3]β‡’[1] ∘ [4]β‡’[3] ,
  [6]β‡’[4] ∘ [2]β‡’[6] ∘ [1]β‡’[2] ∘ [3]β‡’[1] ∘ [5]β‡’[3]) ,
 ([2]β‡’[6] ∘ [1]β‡’[2] ∘ [3]β‡’[1] ∘ [5]β‡’[3] , [6]β‡’[5])
 where
  [1]β‡’[2] : WEM 𝓀 β†’ typal-WEM 𝓀
  [1]β‡’[2] = WEM-gives-typal-WEM fe'
  [2]β‡’[6] : typal-WEM 𝓀 β†’ untruncated-typal-De-Morgan 𝓀
  [2]β‡’[6] = typal-WEM-gives-untruncated-typal-De-Morgan
  [6]β‡’[4] : untruncated-typal-De-Morgan 𝓀 β†’ typal-De-Morgan pt 𝓀
  [6]β‡’[4] = untruncated-typal-De-Morgan-gives-typal-De-Morgan pt
  [6]β‡’[5] : untruncated-typal-De-Morgan 𝓀 β†’ untruncated-De-Morgan 𝓀
  [6]β‡’[5] = untruncated-typal-De-Morgan-gives-untruncated-De-Morgan
  [5]β‡’[3] : untruncated-De-Morgan 𝓀 β†’ De-Morgan pt 𝓀
  [5]β‡’[3] = untruncated-De-Morgan-gives-De-Morgan pt
  [4]β‡’[3] : typal-De-Morgan pt 𝓀 β†’ De-Morgan pt 𝓀
  [4]β‡’[3] = typal-De-Morgan-gives-De-Morgan pt
  [3]β‡’[1] : De-Morgan pt 𝓀 β†’ WEM 𝓀
  [3]β‡’[1] = De-Morgan-gives-WEM pt fe'

Theorem-5-2-ii : is-prop (WEM 𝓀)
               Γ— is-prop (typal-WEM 𝓀)
               Γ— is-prop (De-Morgan pt 𝓀)
               Γ— is-prop (typal-De-Morgan pt 𝓀)
Theorem-5-2-ii = WEM-is-prop fe ,
                 typal-WEM-is-prop fe ,
                 De-Morgan-is-prop pt fe ,
                 typal-De-Morgan-is-prop pt fe

Lemma-5-3 : (Ξ΄ : untruncated-De-Morgan 𝓀)
          β†’ Ξ£ Ξ΄' κž‰ untruncated-De-Morgan 𝓀 , Ξ΄' β‰  Ξ΄
Lemma-5-3 = untruncated-De-Morgan-has-at-least-two-witnesses-if-it-has-one fe'

\end{code}

Section 6. A Rice-like theorem for injective types

\begin{code}

Definition-6-1 : 𝓀 Μ‡  β†’ 𝓀 Μ‡
Definition-6-1 = decomposition

Lemma-6-2 : (X : 𝓀 Μ‡ ) β†’ (Ξ£ Y κž‰ (𝟚 β†’ 𝓀 Μ‡ ) , Y β‚€ + Y ₁ ≃ X) ≃ (X β†’ 𝟚)
Lemma-6-2 {𝓀} = decomposition-lemma (ua 𝓀)

Remark-6-3 : (X : 𝓀 Μ‡ )
           β†’ (decomposition X ≃ (Ξ£ Y κž‰ (𝟚 β†’ 𝓀 Μ‡ ) , (Y β‚€ + Y ₁ ≃ X) Γ— Y β‚€ Γ— Y ₁))
           Γ— (decomposition X ≃ retract 𝟚 of X)
Remark-6-3 {𝓀} X = decompositions-agree (ua 𝓀) X ,
                   decompositions-as-retracts X

Proposition-6-4 : typal-WEM 𝓀 β†’ (X : 𝓀 Μ‡ )
                β†’ has-two-distinct-points X β†’ decomposition X
Proposition-6-4 = WEM-gives-decomposition-of-two-pointed-types

Definition-6-5-i : {𝓀 π“₯ : Universe} β†’ (X : π“₯ Μ‡ ) β†’ X β†’ X β†’ 𝓀 ⁺ βŠ” π“₯ Μ‡
Definition-6-5-i {𝓀} {π“₯} X = Ξ©-Path {π“₯} {X} 𝓀

Definition-6-5-ii : {𝓀 π“₯ : Universe} β†’ (X : π“₯ Μ‡ ) β†’ 𝓀 ⁺ βŠ” π“₯ Μ‡
Definition-6-5-ii {𝓀} {π“₯} = has-Ξ©-paths 𝓀

Lemma-6-6 : decomposition (Ξ© 𝓀) β†’ typal-WEM 𝓀
Lemma-6-6 = decomposition-of-Ξ©-gives-WEM pe'

Lemma-6-7 : (X : 𝓀 Μ‡ ) β†’ decomposition X β†’ has-Ξ©-paths π“₯ X β†’ typal-WEM π“₯
Lemma-6-7 X = decomposition-of-type-with-Ξ©-paths-gives-WEM pe' {X}

Lemma-6-8 : (D : 𝓀 Μ‡ ) β†’ ainjective-type D 𝓀₀ (𝓦 ⁺) β†’ has-Ξ©-paths 𝓦 D
Lemma-6-8 = ainjective-types-have-Ξ©-paths-naive pe'

Lemma-6-9 : (D : 𝓀 Μ‡ ) β†’ ainjective-type D π“₯ 𝓦 β†’ has-Ξ©-paths π“₯ D
Lemma-6-9 = ainjective-types-have-Ξ©-paths pe'

Theorem-6-10 : (D : 𝓀 Μ‡ ) β†’ ainjective-type D π“₯ 𝓦 β†’ decomposition D β†’ typal-WEM π“₯
Theorem-6-10 = decomposition-of-ainjective-type-gives-WEM pe'

Proposition-6-11 : (D : 𝓀 Μ‡ ) β†’ ainjective-type D 𝓀 π“₯
                 β†’ has-two-distinct-points D
                 β†’ decomposable D ↔ decomposition D
Proposition-6-11 D ainj htdp =
 ainjective-type-decomposability-gives-decomposition pe' D ainj htdp , ∣_∣

\end{code}

Section 7. Counterexamples

\begin{code}

Counterexample-7-1 : ainjective-type 𝟚 𝓀 𝓀 ↔ typal-WEM 𝓀
Counterexample-7-1 = 𝟚-ainjective-gives-WEM , WEM-gives-𝟚-ainjective

Lemma-7-2 : WLPO ↔ (Ξ£ f κž‰ (β„•βˆž β†’ β„•βˆž) , ((n : β„•) β†’ f (ΞΉ n) ＝ ΞΉ 0) Γ— (f ∞ ＝ ΞΉ 1))
Lemma-7-2 = WLPO-is-discontinuous' ,
            (Ξ» (f , p) β†’ basic-discontinuity-taboo' f p)

Counterexample-7-3-1 : ainjective-type β„•βˆž 𝓀₀ 𝓀₀ β†’ WLPO
Counterexample-7-3-1 = β„•βˆž-injective-gives-WLPO

Counterexample-7-3-2 : ainjective-type β„•βˆž 𝓀 π“₯ β†’ typal-WEM 𝓀
Counterexample-7-3-2 = β„•βˆž-injective-gives-WEM

Counterexample-7-4-1 : ainjective-type ℝ 𝓀₁ 𝓀₁
                     β†’ Ξ£ H κž‰ (ℝ β†’ ℝ) ,
                           ((x : ℝ) β†’ (x < 0ℝ β†’ H x ＝ 0ℝ)
                                    Γ— (x β‰₯ 0ℝ β†’ H x ＝ 1ℝ))
Counterexample-7-4-1 = ℝ-ainjective-gives-Heaviside-function

Counterexample-7-4-2 : ainjective-type ℝ 𝓀 π“₯ β†’ typal-WEM 𝓀
Counterexample-7-4-2 = ℝ-ainjective-gives-WEM

Definition-7-5 : 𝓀 Μ‡ β†’ (π“₯ : Universe) β†’ π“₯ ⁺ βŠ” 𝓀 Μ‡
Definition-7-5 = Nontrivial-Apartness

Theorem-7-6 : (X : 𝓀 Μ‡ )
            β†’ ainjective-type X 𝓣 𝓦
            β†’ Nontrivial-Apartness X π“₯
            β†’ typal-WEM 𝓣
Theorem-7-6 X = ainjective-type-with-non-trivial-apartness-gives-WEM

Theorem-7-7-1 : typal-WEM 𝓀 β†’ (X : 𝓀 Μ‡ )
              β†’ has-two-distinct-points X
              β†’ Nontrivial-Apartness X 𝓀
Theorem-7-7-1 wem X htdp =
 WEM-gives-that-type-with-two-distinct-points-has-nontrivial-apartness
  fe' {X} htdp wem

Theorem-7-7-2 : typal-WEM 𝓀 β†’ (X : 𝓀 ⁺ Μ‡ )
              β†’ is-locally-small X
              β†’ has-two-distinct-points X
              β†’ Nontrivial-Apartness X 𝓀
Theorem-7-7-2 wem X X-loc-small htdp =
 WEM-gives-that-type-with-two-distinct-points-has-nontrivial-apartness⁺
  fe' X-loc-small htdp wem

Corollary-7-8 : Nontrivial-Apartness (𝓀 Μ‡ ) 𝓀 ↔ typal-WEM 𝓀
Corollary-7-8 {𝓀} =
 Theorem-7-6 (𝓀 Μ‡ ) (universes-are-ainjective-Ξ ' (ua 𝓀)) ,
 (Ξ» wem β†’ Theorem-7-7-2 wem (𝓀 Μ‡ )
                        (universes-are-locally-small (ua 𝓀))
                        universe-has-two-distinct-points)

Corollary-7-9 : (X : 𝓀₀ Μ‡) β†’ simple-typeβ‚‚ X
              β†’ ainjective-type X 𝓀 𝓀 β†’ typal-WEM 𝓀
Corollary-7-9 = simple-typeβ‚‚-injective-gives-WEM

Theorem-7-10 : (X : 𝓀 Μ‡ ) β†’ Tight-Apartness X π“₯ Γ— Β¬ (is-subsingleton X)
             β†’ ainjective-type X 𝓣 𝓦 β†’ ¬¬ typal-WEM 𝓣
Theorem-7-10 X (ta , ns) ainj =
 non-trivial-ainjective-type-with-tight-apartness-gives-¬¬-WEM
  (X , ns , ainj , ta)

Proposition-7-11 : (X : 𝓀 Μ‡ ) β†’ is-totally-separated X Γ— Β¬ (is-subsingleton X)
                 β†’ ainjective-type X 𝓣 𝓦 β†’ ¬¬ typal-WEM 𝓣
Proposition-7-11 X (ts , ns) ainj =
 non-trivial-totally-separated-ainjective-type-gives-¬¬-WEM pe' (X , ns , ts , ainj)

Proposition-7-11-alt : (X : 𝓀 Μ‡ ) β†’ is-totally-separated X Γ— Β¬ (is-subsingleton X)
                     β†’ ainjective-type X 𝓣 𝓦 β†’ ¬¬ typal-WEM 𝓣
Proposition-7-11-alt X (ts , ns) ainj =
 non-trivial-totally-separated-ainjective-type-gives-¬¬-WEM' (X , ns , ts , ainj)

Theorem-7-12 : retracts-of-small-types-are-small
             β†’ (D : 𝓀 Μ‡ )
             β†’ ainjective-type D (𝓀 βŠ” π“₯) 𝓦
             β†’ has-two-distinct-points D
             β†’ is-small (ꪪ 𝓀)
Theorem-7-12 {𝓀} {π“₯} {𝓦} =
 small-ainjective-type-with-two-distinct-points-gives-ꪪ-resizing {𝓀} {π“₯} {𝓦}

Theorem-7-13
 : (ainjective-type (Inhabited 𝓀) 𝓀 𝓀 ↔ retract (Inhabited 𝓀) of (𝓀 Μ‡ ))
 Γ— (retract (Inhabited 𝓀) of (𝓀 Μ‡ ) ↔ Propositions-Are-Projective 𝓀)
 Γ— (Propositions-Are-Projective 𝓀 ↔ Unspecified-Split-Support 𝓀)
Theorem-7-13 {𝓀} =
 ([4]β‡’[2] ∘ [3]β‡’[4] ∘ [1]β‡’[3] , [2]β‡’[1]) ,
 ([1]β‡’[3] ∘ [2]β‡’[1] , [4]β‡’[2] ∘ [3]β‡’[4]) ,
 ([3]β‡’[4] , [1]β‡’[3] ∘ [2]β‡’[1] ∘ [4]β‡’[2])
 where
  [4]β‡’[2] : Unspecified-Split-Support 𝓀 β†’ retract (Inhabited 𝓀) of (𝓀 Μ‡ )
  [4]β‡’[2] = unspecified-split-support-gives-retract 𝓀
  [2]β‡’[1] : retract (Inhabited 𝓀) of (𝓀 Μ‡ ) β†’ ainjective-type (Inhabited 𝓀) 𝓀 𝓀
  [2]β‡’[1] = retract-gives-injectivity 𝓀
  [1]β‡’[3] : ainjective-type (Inhabited 𝓀) 𝓀 𝓀 β†’ Propositions-Are-Projective 𝓀
  [1]β‡’[3] = injectivity-gives-projective-propositions 𝓀
  [3]β‡’[4] : Propositions-Are-Projective 𝓀 β†’ Unspecified-Split-Support 𝓀
  [3]β‡’[4] = projective-propositions-gives-unspecified-split-support 𝓀

Lemma-7-14 : (D : 𝓀 Μ‡ ) β†’ ainjective-type D π“₯ 𝓦 β†’ (T : D β†’ 𝓣 Μ‡ )
           β†’ ainjective-type (Ξ£ d κž‰ D , βˆ₯ T d βˆ₯) (𝓣 βŠ” π“₯') 𝓦'
           β†’ (d : D) β†’ βˆ₯ has-split-support (T d) βˆ₯
Lemma-7-14 {𝓀} {π“₯} {𝓦} {𝓣} {π“₯'} {𝓦'} =
 family-has-unspecified-split-support-if-total-space-of-truncation-is-ainjective
  {𝓀} {π“₯} {𝓦} {𝓣} {π“₯'} {𝓦'}

Lemma-7-15 : WSAC 𝓀 𝓀 ≃ ((X : 𝓀 Μ‡ ) β†’ βˆ₯ has-split-support (X ≃ 𝟚) βˆ₯)
Lemma-7-15 = WSAC-equivalent-formulations

NB : ((X : 𝓀 Μ‡ ) β†’ βˆ₯ has-split-support (X ≃ 𝟚) βˆ₯) ＝ WSAC' 𝓀
NB = refl

Theorem-7-16 : ainjective-type ℝP∞ π“₯ 𝓦 β†’ WSAC' 𝓀₀
Theorem-7-16 = ℝP∞-ainjective-implies-WSAC

\end{code}