Tom de Jong & MartΓ­n EscardΓ³, 8 & 10 September 2023.
Moved to its own file on 29 October 2025.

The type of non-empty types is injective. This should be contrasted with the
fact that the type of inhabited types is not necessarily injective, see
InjectiveTypes.InhabitedTypesTaboo.

An alternative proof of the injectivity of the type of non-empty types
may be found in InjectiveTypes.MathematicalStrutures.

\begin{code}

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

open import MLTT.Spartan
open import UF.Univalence
open import UF.PropTrunc

module InjectiveTypes.NonEmptyTypes
        (pt : propositional-truncations-exist)
        (ua : Univalence)
        (𝓀 : Universe)
       where

open PropositionalTruncation pt

open import UF.Equiv
open import UF.EquivalenceExamples
open import UF.FunExt
open import UF.Retracts
open import UF.Subsingletons
open import UF.Subsingletons-FunExt
open import UF.UA-FunExt

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 InjectiveTypes.Blackboard fe

Non-Empty : 𝓀 ⁺ Μ‡
Non-Empty = Ξ£ X κž‰ 𝓀 Μ‡ , is-nonempty X

Non-Empty-retract : retract Non-Empty of (𝓀 Μ‡ )
Non-Empty-retract = ρ , Οƒ , ρσ
 where
  ρ : 𝓀 Μ‡ β†’ Non-Empty
  ρ X = (¬¬ X β†’ X) , double-negation-elimination-inside-double-negation X
  Οƒ : Non-Empty β†’ 𝓀 Μ‡
  Οƒ = pr₁
  ρσ : ρ ∘ Οƒ ∼ id
  ρσ (X , X-non-empty) = to-subtype-＝ (Ξ» Y β†’ negations-are-props fe')
                                       (eqtoid (ua 𝓀) (¬¬ X β†’ X) X e)
   where
    e = (¬¬ X β†’ X) β‰ƒβŸ¨ I ⟩
        (πŸ™{𝓀} β†’ X) β‰ƒβŸ¨ ≃-sym (πŸ™β†’ fe') ⟩
        X          β– 
     where
      I = β†’cong'' fe' fe' (idtoeq (¬¬ X) πŸ™ II)
       where
        II : ¬¬ X ＝ πŸ™
        II = holds-gives-equal-πŸ™ pe' (¬¬ X) (negations-are-props fe') X-non-empty

Non-Empty-is-injective : ainjective-type Non-Empty 𝓀 𝓀
Non-Empty-is-injective =
 retract-of-ainjective Non-Empty (𝓀 Μ‡ )
                       (universes-are-ainjective (ua 𝓀))
                       Non-Empty-retract

\end{code}