Martin Escardo, 16th August 2023, with more improvements 18th June 2025.

Injectivity of types of mathematical structures, such as pointed
types, ∞-magmas, magmas, monoids, groups etc.

We give a sufficient condition for types of mathematical structures to
be injective, and we apply it to examples such as the above.

This file generalizes InjectiveTypes.MathematicalStructures at the
cost of perhaps being harder to understand. It relies on the file
InjectiveTypes.Sigma, which also arises as a generalization of the
above original file.

Added 5 November 2025 by Tom de Jong: The type of metric spaces is
injective and this relies on the generalizations developed here. This
is the first example that make uses of the added generality of this file.

\begin{code}

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

import InjectiveTypes.MathematicalStructures -- For comparison only.

open import UF.Univalence

\end{code}

We assume univalence (and hence function extensionality, which,
follows from it), but no other HoTT/UF extensions, not even
propositional truncations.

\begin{code}

module InjectiveTypes.MathematicalStructuresMoreGeneral
        (ua : Univalence)
       where

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

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

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

open import InjectiveTypes.Blackboard fe
open import InjectiveTypes.Sigma fe
open import MLTT.Spartan
open import Taboos.Decomposability fe
open import UF.Base
open import UF.Equiv
open import UF.ClassicalLogic
open import UF.PropIndexedPiSigma
open import UF.Retracts
open import UF.Sets
open import UF.Sets-Properties
open import UF.SubtypeClassifier

\end{code}

It is convenient to work with the following definition of (algebraic)
flabbiness of a universe, which uses equivalence of types rather than
equality.

\begin{code}

Flabby : (𝓀 : Universe) β†’ 𝓀 ⁺ Μ‡
Flabby 𝓀 = Ξ£ ⨆ κž‰ ((p : Ξ© 𝓀) β†’ (p holds β†’ 𝓀 Μ‡ ) β†’ 𝓀 Μ‡ )
                , ((p : Ξ© 𝓀) (A : p holds β†’ 𝓀 Μ‡) (h : p holds) β†’ ⨆ p A ≃ A h)

\end{code}

In the presence of univalence we can convert to the usual definition,
and we can always convert in the other direction, but in this file we
need the first one only.

\begin{code}

to-aflabby : Flabby 𝓀 β†’ aflabby (𝓀 Μ‡ ) 𝓀
to-aflabby {𝓀} (⨆ , e) P i A =
 ⨆ (P , i) A , (Ξ» h β†’ eqtoid (ua 𝓀) _ _ (e (P , i) A h))

from-afabbly : aflabby (𝓀 Μ‡ ) 𝓀 β†’ Flabby 𝓀
from-afabbly {𝓀} aflab =
 aflabby-extension aflab ,
 (Ξ» p A h β†’ idtoeq _ _ (aflabby-extension-property aflab p A h))

\end{code}

We already know that universes are flabby in two ways, using ⨆ := Ξ 
and ⨆ := Ξ£, but we give constructions that they are Flabby without
univalence, and hence have better computational behaviour, which will
simplify the applications we have in mind.

If the index type is a proposition, then the projection out of a
Ξ -type is an equivalence.

\begin{code}

Ξ -𝕑𝕣𝕠𝕛 : (p : Ξ© 𝓀) {A : p holds β†’ 𝓀 Μ‡ } (h : p holds)
      β†’ Ξ  A ≃ A h
Ξ -𝕑𝕣𝕠𝕛 p h = Ξ -proj h , Ξ -proj-is-equiv h fe' (holds-is-prop p)

universes-are-Flabby-Ξ  : Flabby 𝓀
universes-are-Flabby-Ξ  = (Ξ» p A β†’ Ξ  A) ,
                         (Ξ» p A β†’ Ξ -𝕑𝕣𝕠𝕛 p)

universes-are-flabby-Ξ  : aflabby (𝓀  Μ‡) 𝓀
universes-are-flabby-Ξ  = to-aflabby universes-are-Flabby-Ξ 

Ξ£-π•šπ•Ÿ : (p : Ξ© 𝓀) {A : p holds β†’ 𝓀 Μ‡ } (h : p holds)
    β†’ A h ≃ Ξ£ A
Ξ£-π•šπ•Ÿ p h = Ξ£-in h , Ξ£-in-is-equiv h (holds-is-prop p)

universes-are-Flabby-Ξ£ : Flabby 𝓀
universes-are-Flabby-Ξ£ = (Ξ» p A β†’ Ξ£ A) ,
                         (Ξ» p A h β†’ ≃-sym (Ξ£-π•šπ•Ÿ p h))

universes-are-flabby-Ξ£ : aflabby (𝓀  Μ‡) 𝓀
universes-are-flabby-Ξ£ = to-aflabby universes-are-Flabby-Ξ£

\end{code}

We now work with an arbitrary notion S of structure on 𝓀. E.g. for
monoids we will take S X := X β†’ X β†’ X, the type of the multiplication
operation.

\begin{code}

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

\end{code}

By the results of InjectiveTypes.Sigma, we get that Ξ£ S is aflabby in
two ways, assuming the compatibility condition for the flabbiness
data.

\begin{code}

 module _ (Ο• : aflabby (𝓀 Μ‡ ) 𝓀) where

  aflabbiness-of-type-of-structured-types : compatibility-data S Ο•
                                          β†’ aflabby (Ξ£ S) 𝓀
  aflabbiness-of-type-of-structured-types = Ξ£-is-aflabby S Ο•

  ainjectivity-of-type-of-structures : compatibility-data S Ο•
                                     β†’ ainjective-type (Ξ£ S) 𝓀 𝓀
  ainjectivity-of-type-of-structures = aflabby-types-are-ainjective (Ξ£ S)
                                       ∘ aflabbiness-of-type-of-structured-types

\end{code}

We will apply this to get our desired examples with Ο• taken to be the
above canonical Ξ -flabby structure on the universe in most cases, and
at least one with the canonical Ξ£-flabby structure.

Next we want to simplify working with compatibility data (as defined
in the module InjectiveTypes.Sigma), where we avoid transports by
working with the following function treq and suitable choices of T and
T-refl in the examples below. Notice that the definition of treq uses
univalence. The point of T and T-refl below is that they won't use
univalence in our examples of interest, so that they will have a
better computational behaviour than treq.

\begin{code}

 treq : {X Y : 𝓀 Μ‡ } β†’ X ≃ Y β†’ S X β†’ S Y
 treq {X} {Y} 𝕗 = transport S (eqtoid (ua 𝓀) X Y 𝕗)

\end{code}

The main additional work in this file on top of InjectiveTypes.Sigma
is to make it easier to work with the compatibility condition for the
purpose of injectivity of types of mathematical structures.

We work with hypothetical T and T-refl with the following types.

\begin{code}

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

\end{code}

The point is that any such T can be equivalently expressed as a
transport and hence we may apply the theorems of the imported file
InjectiveTypes.Sigma, but it may be easier to check the compatibility
condition using T rather than transport (see examples below).

\begin{code}

  T-is-treq : {X Y : 𝓀 Μ‡ } (𝕗 : X ≃ Y)
            β†’ T 𝕗 ∼ treq 𝕗
  T-is-treq {X} {Y} 𝕗 s = JEq (ua 𝓀) X A I Y 𝕗
   where
    A : (Y : 𝓀 Μ‡ ) (𝕗 : X ≃ Y) β†’ π“₯ Μ‡
    A Y 𝕗 = T 𝕗 s ＝ treq 𝕗 s

    I : A X (≃-refl X)
    I = T (≃-refl X) s                                ＝⟨ T-refl s ⟩
        s                                             ＝⟨ refl ⟩
        transport S refl s                            ＝⟨ II ⟩
        transport S (eqtoid (ua 𝓀) X X (≃-refl X)) s  ＝⟨ refl ⟩
        treq (≃-refl X) s                             ∎
      where
       II = (ap (Ξ» - β†’ transport S - s) (eqtoid-refl (ua 𝓀) X))⁻¹

\end{code}

In order to be able to apply the results of InjectiveTypes.Sigma, we
perform the following construction. That file requires compatibility
data of a certain kind, which we reduce to compatibility of another
kind, which will be easier to produce in our sample applications.

\begin{code}

  module compatibility-data-construction (Ο•@(⨆ , Ξ΅) : Flabby 𝓀) where

   derived-ρ : (p : Ξ© 𝓀)
               (A : p holds β†’ 𝓀 Μ‡ )
             β†’ S (⨆ p A) β†’ ((h : p holds) β†’ S (A h))
   derived-ρ p A s h = T (Ρ p A h) s

   compatibility-data-for-derived-ρ : 𝓀 ⁺ βŠ” π“₯ Μ‡
   compatibility-data-for-derived-ρ = (p : Ξ© 𝓀)
                                      (A : p holds β†’ 𝓀 Μ‡ )
                                    β†’ has-section (derived-ρ p A)

   construction : compatibility-data-for-derived-ρ
                β†’ compatibility-data S (to-aflabby Ο•)
   construction t p A = III
    where

     II : derived-ρ p A ∼ ρ S (to-aflabby Ο•) p A
     II s =
      derived-ρ p A s                                     ＝⟨ refl ⟩
      (Ξ» h β†’ T (Ξ΅ p A h) s)                               ＝⟨ Iβ‚€ ⟩
      (Ξ» h β†’ treq (Ξ΅ p A h) s)                            ＝⟨ refl ⟩
      (Ξ» h β†’ transport S (eqtoid (ua 𝓀) _ _ (Ξ΅ p A h)) s) ＝⟨ refl ⟩
      ρ S (to-aflabby Ο•) p A s                           ∎
      where
       Iβ‚€ = dfunext fe' (Ξ» h β†’ T-is-treq (Ξ΅ p A h) s)

     III : has-section (ρ S (to-aflabby Ο•) p A)
     III = has-section-closed-under-∼ (derived-ρ p A) _ (t p A) (∼-sym II)

\end{code}

This completes the construction, but we record that the section map of
the above construction is literally the same as that of the
hypothesis t.

\begin{code}

     _ = section-map (ρ S (to-aflabby Ο•) p A) III  ＝⟨ refl ⟩
         section-map (derived-ρ p A) (t p A)        ∎

\end{code}

What is necessarily different is the proof that this map is a
section. In fact, it is different in the strong sense that the
comparison for equality doesn't even make sense - it wouldn't even
typecheck.

A way to verify this in Agda is to try to supply the following naive
definition.

   construction' : compatibility-data-for-derived-ρ
                 β†’ compatibility-data S (to-aflabby Ο•)
   construction' t = t -- Doesn't type check (of course).

We can sensibly have only that the *section map* of the construction
agrees with the given section map, which is what we have already
observed in the above proof, but record again with full type
information, outside the above proof.

\begin{code}

   construction-fact : (p : Ξ© 𝓀)
                       (A : p holds β†’ 𝓀 Μ‡)
                       (t : compatibility-data-for-derived-ρ)
                     β†’ section-map (ρ S (to-aflabby Ο•) p A) (construction t p A)
                     ＝ section-map (derived-ρ p A)         (t p A)
   construction-fact p A t = refl

\end{code}

This fact about the construction will be rather useful in practice,
for the applications we have in mind.

We can specialize this to the Ξ  and Ξ£ flabbiness structures discussed
above, to get the following.

\begin{code}

  module _ where

   open compatibility-data-construction universes-are-Flabby-Ξ 

   ρΠ : (p : Ξ© 𝓀)
        (A : p holds β†’ 𝓀 Μ‡ )
      β†’ S (Ξ  A) β†’ ((h : p holds) β†’ S (A h))
   ρΠ = derived-ρ

   compatibility-data-Ξ  : 𝓀 ⁺ βŠ” π“₯ Μ‡
   compatibility-data-Ξ  = (p : Ξ© 𝓀)
                          (A : p holds β†’ 𝓀 Μ‡ )
                        β†’ has-section (ρΠ p A)

   Ξ -construction : compatibility-data-Ξ 
                  β†’ compatibility-data S universes-are-flabby-Ξ 
   Ξ -construction = construction

\end{code}

We use the following definitional equality a number of times (and we
try to record this explicitly when we do so).

\begin{code}

   _ : ρΠ ＝ Ξ» p A s h β†’ T (Ξ -𝕑𝕣𝕠𝕛 p h) s
   _ = refl

\end{code}

For most examples below, we only need the above functions ρΠ,
compatibility-data-Ξ  and Ξ -construction, but at least one of them uses
their Ξ£ versions defined below.

\begin{code}

  module _ where

   open compatibility-data-construction universes-are-Flabby-Ξ£

   ρΣ : (p : Ξ© 𝓀)
        (A : p holds β†’ 𝓀 Μ‡ )
      β†’ S (Ξ£ A) β†’ ((h : p holds) β†’ S (A h))
   ρΣ = derived-ρ

   compatibility-data-Ξ£ : 𝓀 ⁺ βŠ” π“₯ Μ‡
   compatibility-data-Ξ£ = (p : Ξ© 𝓀)
                          (A : p holds β†’ 𝓀 Μ‡ )
                        β†’ has-section (ρΣ p A)

   Ξ£-construction : compatibility-data-Ξ£
                  β†’ compatibility-data S universes-are-flabby-Ξ£
   Ξ£-construction = construction

\end{code}

Example. The type of pointed types is algebraically injective. We use
the Ξ -flabbiness of the universe.

\begin{code}

Pointed-type : (𝓀 : Universe) β†’ 𝓀 ⁺ Μ‡
Pointed-type 𝓀 = Ξ£ X κž‰ 𝓀 Μ‡ , X

Pointed : 𝓀 Μ‡ β†’ 𝓀 Μ‡
Pointed X = X

Pointed-Ξ -data : compatibility-data (Pointed {𝓀}) universes-are-flabby-Ξ 
Pointed-Ξ -data {𝓀} = Ξ -construction Pointed T T-refl c
 where
  S = Pointed

  T : {X Y : 𝓀 Μ‡ } β†’ (X ≃ Y) β†’ X β†’ Y
  T = ⌜_⌝

  T-refl : {X : 𝓀 Μ‡ } β†’ T (≃-refl X) ∼ id
  T-refl x = refl

  _ : (p : Ξ© 𝓀) (A : p holds β†’ 𝓀 Μ‡) β†’ ρΠ S T T-refl p A ＝ 𝑖𝑑 (S (Ξ  A))
  _ = Ξ» p A β†’ refl

  c : compatibility-data-Ξ  S T T-refl
  c p A = equivs-have-sections id (id-is-equiv (Ξ  A))

\end{code}

Hence we conclude that the type of pointed types is ainjective.

\begin{code}

ainjectivity-of-type-of-pointed-types : ainjective-type (Pointed-type 𝓀) 𝓀 𝓀
ainjectivity-of-type-of-pointed-types =
 ainjectivity-of-type-of-structures
  Pointed
  universes-are-flabby-Ξ 
  Pointed-Ξ -data

\end{code}

Example. The type of ∞-magmas is algebraically injective. The proof is
an entirely routine application of the above general theorem after we
guess what T should be.

\begin{code}

∞-Magma : (𝓀 : Universe) β†’ 𝓀 ⁺ Μ‡
∞-Magma 𝓀 = Ξ£ X κž‰ 𝓀 Μ‡ , (X β†’ X β†’ X)

∞-magma-structure : 𝓀 Μ‡ β†’ 𝓀 Μ‡
∞-magma-structure = Ξ» X β†’ X β†’ X β†’ X

∞-Magma-structure-Π-data : compatibility-data
                            (∞-magma-structure {𝓀})
                            universes-are-flabby-Ξ 
∞-Magma-structure-Ξ -data {𝓀} =
 Π-construction S T T-refl ρΠ-has-section
 where
  S = ∞-magma-structure

  T : {X Y : 𝓀 Μ‡ } β†’ (X ≃ Y) β†’ S X β†’ S Y
  T 𝕗 _Β·_ = Ξ» y y' β†’ ⌜ 𝕗 ⌝ (⌜ 𝕗 ⌝⁻¹ y Β· ⌜ 𝕗 ⌝⁻¹ y')

  T-refl : {X : 𝓀 Μ‡ } β†’ T (≃-refl X) ∼ id
  T-refl _Β·_ = refl

  module _ (p : Ξ© 𝓀)
           (A : p holds β†’ 𝓀 Μ‡ )
         where

   Ο€ : (h : p holds) β†’ Ξ  A ≃ A h
   Ο€ = Ξ -𝕑𝕣𝕠𝕛 p

   r : S (Ξ  A) β†’ ((h : p holds) β†’ S (A h))
   r _Β·_ h a b = ⌜ Ο€ h ⌝ (⌜ Ο€ h ⌝⁻¹ a Β· ⌜ Ο€ h ⌝⁻¹ b)

   _ : r ＝ ρΠ S T T-refl p A
   _ = refl -- Which is crucial for the proof below to work.

   Οƒ : ((h : p holds) β†’ S (A h)) β†’ S (Ξ  A)
   Οƒ g Ξ± Ξ² h = g h (⌜ Ο€ h ⌝ Ξ±) (⌜ Ο€ h ⌝ Ξ²)

   rΟƒ : r ∘ Οƒ ∼ id
   rσ g =
    r (Οƒ g)                                                         ＝⟨ refl ⟩
    (Ξ» h a b β†’ g h (⌜ Ο€ h ⌝ (⌜ Ο€ h ⌝⁻¹ a)) (⌜ Ο€ h ⌝ (⌜ Ο€ h ⌝⁻¹ b))) ＝⟨ II ⟩
    (Ξ» h a b β†’ g h a b)                                             ＝⟨ refl ⟩
    g                                                               ∎
     where
      II = dfunext fe' (Ξ» h β†’
           dfunext fe' (Ξ» a β†’
           dfunext fe' (Ξ» b β†’
            apβ‚‚ (g h)
             (inverses-are-sections' (Ο€ h) a)
             (inverses-are-sections' (Ο€ h) b))))

   ρΠ-has-section : has-section (ρΠ S T T-refl p A)
   ρΠ-has-section = Οƒ , rΟƒ

ainjectivity-of-∞-Magma : ainjective-type (∞-Magma 𝓀) 𝓀 𝓀
ainjectivity-of-∞-Magma =
 ainjectivity-of-type-of-structures
  ∞-magma-structure
  universes-are-flabby-Ξ 
  ∞-Magma-structure-Π-data

\end{code}

A corollary is that the type ∞-Magma 𝓀 doesn't have any non-trivial
decidable property unless weak excluded middle holds.

\begin{code}

decomposition-of-∞-Magma-gives-WEM : decomposition (∞-Magma 𝓀) β†’ typal-WEM 𝓀
decomposition-of-∞-Magma-gives-WEM {𝓀} =
 decomposition-of-ainjective-type-gives-WEM
  (univalence-gives-propext (ua 𝓀))
  (∞-Magma 𝓀)
  ainjectivity-of-∞-Magma

\end{code}

The same is true for the type of pointed types, of course, and for any
injective type.

Example. The type of pointed ∞-magmas is injective.

\begin{code}

open import UF.SIP-Examples
open monoid

∞-Magmaβˆ™ : (𝓀 : Universe) β†’ 𝓀 ⁺ Μ‡
∞-Magmaβˆ™ 𝓀 = Ξ£ X κž‰ 𝓀 Μ‡ , (X β†’ X β†’ X) Γ— X

∞-Magmaβˆ™-structure : 𝓀 Μ‡ β†’ 𝓀 Μ‡
∞-Magmaβˆ™-structure = monoid-structure

∞-Magmaβˆ™-structure-Ξ -data : compatibility-data
                             (∞-Magmaβˆ™-structure {𝓀})
                             universes-are-flabby-Ξ 
∞-Magmaβˆ™-structure-Ξ -data =
 compatibility-data-Γ—
  universes-are-flabby-Ξ 
  ∞-Magma-structure-Π-data
  Pointed-Ξ -data

ainjectivity-of-∞-Magmaβˆ™ : ainjective-type (∞-Magmaβˆ™ 𝓀) 𝓀 𝓀
ainjectivity-of-∞-Magmaβˆ™ =
 ainjectivity-of-type-of-structures
  ∞-Magmaβˆ™-structure
  universes-are-flabby-Ξ 
  ∞-Magmaβˆ™-structure-Ξ -data

\end{code}

Example. The type of monoids is injective. We just have to check that
the monoid axioms are closed under Ξ .

\begin{code}

Monoid-Ξ -data : compatibility-data {𝓀 ⁺}
                 (Ξ» X β†’ Ξ£ s κž‰ monoid-structure X , monoid-axioms X s)
                 universes-are-flabby-Ξ 
Monoid-Ξ -data {𝓀} =
 compatibility-data-with-axioms
  universes-are-flabby-Ξ 
  monoid-structure
  ∞-Magmaβˆ™-structure-Ξ -data
  monoid-axioms
  (monoid-axioms-is-prop fe')
  axioms-Ξ -data
 where
  Οƒ : (p : Ξ© 𝓀) (A : p holds β†’ 𝓀 Μ‡ )
    β†’ ((h : p holds) β†’ monoid-structure (A h)) β†’ monoid-structure (Ξ  A)
  Οƒ p A = section-map
           (ρ monoid-structure universes-are-flabby-Π p A)
           (∞-Magmaβˆ™-structure-Ξ -data p A)

  axioms-Ξ -data
   : (p : Ξ© 𝓀)
     (A : p holds β†’ 𝓀 Μ‡ )
     (Ξ± : (h : p holds) β†’ monoid-structure (A h))
     (F : (h : p holds) β†’ monoid-axioms (A h) (Ξ± h))
   β†’ monoid-axioms (Ξ  A) (Οƒ p A Ξ±)
  axioms-Ξ -data p A Ξ± F = I , II , III , IV
   where
    _*_ : {h : p holds} β†’ A h β†’ A h β†’ A h
    _*_ {h} = pr₁ (Ξ± h)

    _Β·_ : Ξ  A β†’ Ξ  A β†’ Ξ  A
    (f Β· g) h = f h * g h

    e : Ξ  A
    e h = prβ‚‚ (Ξ± h)

    _ : Οƒ p A Ξ± ＝ (_Β·_ , e)
    _ = refl -- Which is crucial for the proof below to work.

    I : is-set (Ξ  A)
    I = Ξ -is-set fe' (Ξ» h β†’
         case F h of
          Ξ» (Ah-is-set , ln , rn , assoc) β†’ Ah-is-set)

    II : left-neutral e _Β·_
    II f = dfunext fe' (Ξ» h β†’
            case F h of
             Ξ» (Ah-is-set , ln , rn , assoc) β†’ ln (f h))

    III : right-neutral e _Β·_
    III g = dfunext fe' (Ξ» h β†’
             case F h of
              Ξ» (Ah-is-set , ln , rn , assoc) β†’ rn (g h))

    IV : associative _Β·_
    IV f g k = dfunext fe' (Ξ» h β†’
                case F h of
                 Ξ» (Ah-is-set , ln , rn , assoc) β†’ assoc (f h) (g h) (k h))

ainjectivity-of-Monoid : ainjective-type (Monoid {𝓀}) 𝓀 𝓀
ainjectivity-of-Monoid {𝓀} =
 ainjectivity-of-type-of-structures
  (Ξ» X β†’ Ξ£ s κž‰ monoid-structure X , monoid-axioms X s)
  universes-are-flabby-Ξ 
  Monoid-Ξ -data

\end{code}

It is easy to add further axioms to monoids to get groups, and then
show that the type of groups is injective using the above
technique. This is just as routine as the example of monoids. All one
needs to do is to show that the group axioms are closed under
prop-indexed products.

TODO. Maybe implement this.

NB. The type Ordinal 𝓀 of well-ordered sets in 𝓀 is also injective,
but for different reasons, two of them given in two different modules.

Added 20th June 2025. The type of all families in a universe is
injective.

\begin{code}

Fam : (𝓀 : Universe) β†’ 𝓀 ⁺ Μ‡
Fam 𝓀 = Ξ£ X κž‰ 𝓀 Μ‡ , (X β†’ 𝓀 Μ‡)

Fam-structure : 𝓀 Μ‡ β†’ 𝓀 ⁺ Μ‡
Fam-structure {𝓀} X = X β†’ 𝓀 Μ‡

open import UF.EquivalenceExamples
open import UF.Subsingletons

Fam-Ξ -data : compatibility-data (Fam-structure {𝓀}) universes-are-flabby-Ξ 
Fam-Ξ -data {𝓀} = Ξ -construction Fam-structure T T-refl c
 where
  S = Fam-structure

  T : {X Y : 𝓀 Μ‡} β†’ X ≃ Y β†’ (X β†’ 𝓣 Μ‡ ) β†’ (Y β†’ 𝓣 Μ‡ )
  T 𝕗 R = Ξ» y β†’ R (⌜ 𝕗 ⌝⁻¹ y)

  T-refl : {X : 𝓀 Μ‡} β†’ T (≃-refl X) ∼ id
  T-refl R = refl

  module _ (p : Ξ© 𝓀) (A : p holds β†’ 𝓀 Μ‡) where

   r :  S (Ξ  A) β†’ ((h : p holds) β†’ S (A h))
   r s h a = s (⌜ Ξ -𝕑𝕣𝕠𝕛 p h ⌝⁻¹ a)

   _ : ρΠ S T T-refl p A ＝ r
   _ = refl

   Οƒ : ((h : p holds) β†’ S (A h)) β†’ S (Ξ  A)
   Οƒ g f = (h : p holds) β†’ g h (f h)

   rΟƒ : r ∘ Οƒ ∼ id
   rσ g = dfunext fe' (λ h → dfunext fe' (II h))
    where
     module _ (h : p holds) (a : A h) where

      Ο€ : Ξ  A ≃ A h
      Ο€ = Ξ -𝕑𝕣𝕠𝕛 p h

      I = ((h' : p holds) β†’ g h' (⌜ Ο€ ⌝⁻¹ a h')) β‰ƒβŸ¨ Iβ‚€ ⟩
          (p holds β†’ g h (⌜ Ο€ ⌝⁻¹ a h))          β‰ƒβŸ¨ I₁ ⟩
          (πŸ™ β†’ g h (⌜ Ο€ ⌝⁻¹ a h))                β‰ƒβŸ¨ Iβ‚‚ ⟩
          g h (⌜ Ο€ ⌝⁻¹ a h)                      β– 
        where
         Iβ‚€ = Ξ -cong fe' fe'
               (Ξ» h' β†’ transport (Ξ» - β†’ g - (⌜ Ο€ ⌝⁻¹ a -))
                                 (holds-is-prop p h' h) ,
                       transports-are-equivs (holds-is-prop p h' h))
         I₁ = Ξ -change-of-variable-≃ {𝓀} {𝓀} fe
               (Ξ» _ β†’ g h (⌜ Ο€ ⌝⁻¹ a h))
               (logically-equivalent-props-are-equivalent
                 (holds-is-prop p) πŸ™-is-prop unique-to-πŸ™ (Ξ» _ β†’ h))
         Iβ‚‚ = ≃-sym (πŸ™β†’ fe')

      II = r (Οƒ g) h a                            ＝⟨ refl ⟩
           Οƒ g (⌜ Ο€ ⌝⁻¹ a)                        ＝⟨ refl ⟩
           ((h' : p holds) β†’ g h' (⌜ Ο€ ⌝⁻¹ a h')) ＝⟨ IIβ‚€ ⟩
           g h (⌜ Ο€ ⌝⁻¹ a h)                      ＝⟨ refl ⟩
           g h (⌜ Ο€ ⌝ (⌜ Ο€ ⌝⁻¹ a))                ＝⟨ II₁ ⟩
           g h a                                  ∎
            where
             IIβ‚€  = eqtoid (ua 𝓀) _ _ I
             II₁ = ap (g h) (inverses-are-sections' Ο€ a)

  c :  compatibility-data-Ξ  Fam-structure T T-refl
  c p A = σ p A , rσ p A

ainjectivity-of-Fam : ainjective-type (Fam 𝓀) 𝓀 𝓀
ainjectivity-of-Fam =
 ainjectivity-of-type-of-structures
  Fam-structure
  universes-are-flabby-Ξ 
  Fam-Ξ -data

\end{code}

A corollary is that the type of all functions in a universe is injective.

\begin{code}

open import UF.Classifiers

ainjectivity-of-type-of-all-functions
 : ainjective-type (Ξ£ X κž‰ 𝓀 Μ‡ , Ξ£ Y κž‰ 𝓀 Μ‡ , (X β†’ Y)) 𝓀 𝓀
ainjectivity-of-type-of-all-functions {𝓀}
 = transport
    (Ξ» - β†’ ainjective-type - 𝓀 𝓀)
    (eqtoid (ua (𝓀 ⁺)) _ _ (≃-sym I))
    ainjectivity-of-Fam
 where
  open classifier-single-universe 𝓀

  I = (Ξ£ X κž‰ 𝓀 Μ‡ , Ξ£ Y κž‰ 𝓀 Μ‡ , (X β†’ Y)) β‰ƒβŸ¨ Ξ£-flip ⟩
      (Ξ£ Y κž‰ 𝓀 Μ‡ , Ξ£ X κž‰ 𝓀 Μ‡ , (X β†’ Y)) β‰ƒβŸ¨ Ξ£-cong (classification (ua 𝓀) fe') ⟩
      (Ξ£ Y κž‰ 𝓀 Μ‡ , (Y β†’ 𝓀 Μ‡))           β‰ƒβŸ¨ ≃-refl _ ⟩
      Fam 𝓀                           β– 

\end{code}

The type of all type-valued relations, or multigraphs, in a universe
is injective. The proof is the binary version of the above unary proof.

\begin{code}

Graph : (𝓀 : Universe) β†’ 𝓀 ⁺ Μ‡
Graph 𝓀 = Ξ£ X κž‰ 𝓀 Μ‡ , (X β†’ X β†’ 𝓀 Μ‡)

graph-structure : 𝓀 Μ‡ β†’ 𝓀 ⁺ Μ‡
graph-structure {𝓀} X = X β†’ X β†’ 𝓀 Μ‡

open import UF.EquivalenceExamples
open import UF.Subsingletons

Graph-Ξ -data : compatibility-data (graph-structure {𝓀}) universes-are-flabby-Ξ 
Graph-Ξ -data {𝓀} =
 Ξ -construction graph-structure T T-refl c
 where
  S = graph-structure

  T : {X Y : 𝓀 Μ‡} β†’ X ≃ Y β†’ (X β†’ X β†’ 𝓣 Μ‡ ) β†’ (Y β†’ Y β†’ 𝓣 Μ‡ )
  T 𝕗 R y y' = R (⌜ 𝕗 ⌝⁻¹ y) (⌜ 𝕗 ⌝⁻¹ y')

  T-refl : {X : 𝓀 Μ‡} β†’ T (≃-refl X) ∼ id
  T-refl R = refl

  module _ (p : Ξ© 𝓀) (A : p holds β†’ 𝓀 Μ‡) where

   r :  S (Ξ  A) β†’ ((h : p holds) β†’ S (A h))
   r s h a a' = s (⌜ Ξ -𝕑𝕣𝕠𝕛 p h ⌝⁻¹ a) (⌜ Ξ -𝕑𝕣𝕠𝕛 p h ⌝⁻¹ a')

   _ : r ＝ ρΠ S T T-refl p A
   _ = refl

   Οƒ : ((h : p holds) β†’ S (A h)) β†’ S (Ξ  A)
   Οƒ g f f' = (h : p holds) β†’ g h (f h) (f' h)

   rΟƒ : r ∘ Οƒ ∼ id
   rσ g = dfunext fe' (λ h →
          dfunext fe' (Ξ» a β†’
          dfunext fe' (Ξ» a' β†’ II h a a')))
    where
     module _ (h : p holds) (a a' : A h) where

      Ο€ : Ξ  A ≃ A h
      Ο€ = Ξ -𝕑𝕣𝕠𝕛 p h

      I = ((h' : p holds) β†’ g h' (⌜ Ο€ ⌝⁻¹ a h') (⌜ Ο€ ⌝⁻¹ a' h')) β‰ƒβŸ¨ Iβ‚€ ⟩
          (p holds β†’ g h (⌜ Ο€ ⌝⁻¹ a h) (⌜ Ο€ ⌝⁻¹ a' h))           β‰ƒβŸ¨ I₁ ⟩
          (πŸ™ β†’ g h (⌜ Ο€ ⌝⁻¹ a h) (⌜ Ο€ ⌝⁻¹ a' h))                 β‰ƒβŸ¨ Iβ‚‚ ⟩
          g h (⌜ Ο€ ⌝⁻¹ a h) (⌜ Ο€ ⌝⁻¹ a' h)                       β– 
        where
         Iβ‚€ = Ξ -cong fe' fe'
               (Ξ» h' β†’ transport (Ξ» - β†’ g - (⌜ Ο€ ⌝⁻¹ a -) (⌜ Ο€ ⌝⁻¹ a' -))
                                 (holds-is-prop p h' h) ,
                       transports-are-equivs (holds-is-prop p h' h))
         I₁ = Ξ -change-of-variable-≃ {𝓀} {𝓀} fe
               (Ξ» _ β†’ g h (⌜ Ο€ ⌝⁻¹ a h) (⌜ Ο€ ⌝⁻¹ a' h))
               (logically-equivalent-props-are-equivalent
                 (holds-is-prop p) πŸ™-is-prop unique-to-πŸ™ (Ξ» _ β†’ h))
         Iβ‚‚ = ≃-sym (πŸ™β†’ fe')

      II = r (Οƒ g) h a a'                                         ＝⟨ refl ⟩
           Οƒ g (⌜ Ο€ ⌝⁻¹ a) (⌜ Ο€ ⌝⁻¹ a')                           ＝⟨ refl ⟩
           ((h' : p holds) β†’ g h' (⌜ Ο€ ⌝⁻¹ a h') (⌜ Ο€ ⌝⁻¹ a' h')) ＝⟨ IIβ‚€ ⟩
           g h (⌜ Ο€ ⌝⁻¹ a h) (⌜ Ο€ ⌝⁻¹ a' h)                       ＝⟨ refl ⟩
           g h (⌜ Ο€ ⌝ (⌜ Ο€ ⌝⁻¹ a)) (⌜ Ο€ ⌝ (⌜ Ο€ ⌝⁻¹ a'))           ＝⟨ II₁ ⟩
           g h a a'                                               ∎
            where
             IIβ‚€  = eqtoid (ua 𝓀) _ _ I
             II₁ = apβ‚‚ (g h)
                       (inverses-are-sections' Ο€ a)
                       (inverses-are-sections' Ο€ a')

  c :  compatibility-data-Ξ  graph-structure T T-refl
  c p A = σ p A , rσ p A

ainjectivity-of-Graph : ainjective-type (Graph 𝓀) 𝓀 𝓀
ainjectivity-of-Graph =
 ainjectivity-of-type-of-structures
  graph-structure
  universes-are-flabby-Ξ 
  Graph-Ξ -data

\end{code}

As a consequence, we get the injectivity of the type of posets.

\begin{code}

poset-axioms : (X : 𝓀 Μ‡ ) β†’ graph-structure X β†’ 𝓀 Μ‡
poset-axioms X _≀_ = is-set X
                   Γ— ((x y : X) β†’ is-prop (x ≀ y))
                   Γ— reflexive     _≀_
                   Γ— transitive    _≀_
                   Γ— antisymmetric _≀_

Poset : (𝓀 : Universe) β†’ 𝓀 ⁺ Μ‡
Poset 𝓀 = Ξ£ X κž‰ 𝓀 Μ‡ , Ξ£ s κž‰ graph-structure X , poset-axioms X s

open import UF.Subsingletons-FunExt

poset-axioms-is-prop : (X : 𝓀 Μ‡ ) (s : graph-structure X)
                     β†’ is-prop (poset-axioms X s)
poset-axioms-is-prop X _≀_ = prop-criterion I
 where
  I : poset-axioms X _≀_ β†’ is-prop (poset-axioms X _≀_)
  I (s , pv , r , t , a) =
   Γ—β‚…-is-prop
    (being-set-is-prop fe')
    (Ξ β‚‚-is-prop fe' (Ξ» x y β†’ being-prop-is-prop fe'))
    (Ξ -is-prop fe' (Ξ» x β†’ pv x x))
    (Ξ β‚…-is-prop fe' (Ξ» x _ z _ _ β†’ pv x z))
    (Ξ β‚„-is-prop fe' (Ξ» _ _ _ _ β†’ s))

Poset-Ξ -data : compatibility-data {𝓀 ⁺}
                 (Ξ» X β†’ Ξ£ s κž‰ graph-structure X , poset-axioms X s)
                 universes-are-flabby-Ξ 
Poset-Ξ -data {𝓀} =
 compatibility-data-with-axioms
  universes-are-flabby-Ξ 
  graph-structure
  Graph-Ξ -data
  poset-axioms
  poset-axioms-is-prop
  axioms-Ξ -data
 where
  Οƒ : (p : Ξ© 𝓀) (A : p holds β†’ 𝓀 Μ‡ )
    β†’ ((h : p holds) β†’ graph-structure (A h)) β†’ graph-structure (Ξ  A)
  Οƒ p A = section-map
           (ρ graph-structure universes-are-flabby-Π p A)
           (Graph-Ξ -data p A)

  axioms-Ξ -data
   : (p : Ξ© 𝓀)
     (A : p holds β†’ 𝓀 Μ‡ )
     (Ξ± : (h : p holds) β†’ graph-structure (A h))
     (F : (h : p holds) β†’ poset-axioms (A h) (Ξ± h))
   β†’ poset-axioms (Ξ  A) (Οƒ p A Ξ±)
  axioms-Ξ -data p A Ξ± F = I , II , III , IV , V
   where
    _βŠ‘_ : {h : p holds} β†’ A h β†’ A h β†’ 𝓀 Μ‡
    _βŠ‘_ {h} = Ξ± h

    _≀_ : Ξ  A β†’ Ξ  A β†’ 𝓀 Μ‡
    f ≀ g = (h : p holds) β†’ f h βŠ‘ g h

    _ : Οƒ p A Ξ± ＝ _≀_
    _ = refl -- Which is crucial for the proof below to work.

    I : is-set (Ξ  A)
    I = Ξ -is-set fe' (Ξ» h β†’
         case F h of
          Ξ» (s , pv , r , t , a) β†’ s)

    II : (f g : Ξ  A) β†’ is-prop (f ≀ g)
    II f g = Ξ -is-prop fe' (Ξ» h β†’
              case F h of
               Ξ» (s , pv , r , t , a) β†’ pv (f h) (g h))

    III : reflexive _≀_
    III f h =
     case F h of
      Ξ» (s , pv , r , t , a) β†’ r (f h)

    IV : transitive _≀_
    IV fβ‚€ f₁ fβ‚‚ l m h =
     case F h of
      Ξ» (s , pv , r , t , a) β†’ t (fβ‚€ h) (f₁ h) (fβ‚‚ h) (l h) (m h)

    V : antisymmetric _≀_
    V fβ‚€ f₁ l m = dfunext fe' (Ξ» h β†’
                   case F h of
                    Ξ» (s , pv , r , t , a) β†’ a (fβ‚€ h) (f₁ h) (l h) (m h))

ainjectivity-of-Poset : ainjective-type (Poset 𝓀) 𝓀 𝓀
ainjectivity-of-Poset {𝓀} =
 ainjectivity-of-type-of-structures
  (Ξ» X β†’ Ξ£ s κž‰ graph-structure X , poset-axioms X s)
  universes-are-flabby-Ξ 
  Poset-Ξ -data

\end{code}

Notice that, just as in the case for monoids, the proof amounts to
showing that posets are closed under prop-indexed products. Using the
same idea, it is straightforward to show that the types of dcpos,
continuous dcpos, suplattices, frames etc. are all injective. (Notice
that this is different from e.g. saying that the underlying type of a
dcpos is injective, which is also true and is proved in another
module.)

TODO. Maybe implement (some of) these examples.

TODO. More techniques are needed to show that the type of 1-categories
would be injective. A category can be seen as a graph equipped with
operations (identity and composition) satisfying properties (identity
laws, associativity, univalence).

Added 24 July 2025 by Tom de Jong.

In InjectiveTypes.InhabitedTypesTaboo we showed that the type of nonempty types
is injective by exhibiting it as a retract of the universe. In line with the
condition from InjectiveTypes.Subtypes, the argument there shows that a type is
nonempty if and only if it is a fixed point of the map X ↦ (¬¬ X β†’ X).

Here is an alternative proof, using that
   (Ξ  (p : P) , ¬¬ A p)   β†’   ¬¬ Ξ  (p : P) , A p
holds when P is a proposition.

\begin{code}

Nonempty-Ξ -data : compatibility-data (is-nonempty {𝓀}) universes-are-flabby-Ξ 
Nonempty-Ξ -data {𝓀} = Ξ -construction is-nonempty T T-refl c
 where
  S = is-nonempty

  T : {X Y : 𝓀 Μ‡ } β†’ (X ≃ Y) β†’ S X β†’ S Y
  T e = ¬¬-functor ⌜ e ⌝

  T-refl : {X : 𝓀 Μ‡ } β†’ T (≃-refl X) ∼ id
  T-refl x = refl

  Οƒ : (p : Ξ© 𝓀) (A : p holds β†’ 𝓀 Μ‡ )
    β†’ ((h : p holds) β†’ S (A h)) β†’ S (Ξ  A)
  Οƒ p A Ο† Ξ½ = III
   where
    I : (h : p holds) β†’ Β¬ A h
    I h a = Ξ½ (Ξ» h' β†’ transport A (holds-is-prop p h h') a)

    II : Β¬ (p holds)
    II h = Ο† h (I h)

    III : 𝟘
    III = Ξ½ (Ξ» h β†’ 𝟘-elim (II h))

  c : compatibility-data-Ξ  S T T-refl
  c p A = Οƒ p A , (Ξ» Ο† β†’ dfunext fe' (Ξ» h β†’ negations-are-props fe' _ _))

ainjectivity-of-type-of-nonempty-types
 : ainjective-type (Ξ£ X κž‰ 𝓀 Μ‡ , is-nonempty X) 𝓀 𝓀
ainjectivity-of-type-of-nonempty-types =
 ainjectivity-of-type-of-structures
  is-nonempty
  universes-are-flabby-Ξ 
  Nonempty-Ξ -data

\end{code}

Added 5 November 2025 by Tom de Jong.

All previous examples used the Ξ -flabbiness structure on the universe. In what
follows we put the extra generality of our machinery to good use by instead
employing the Ξ£-flabbiness structure to prove that the type of metric spaces is
injective.

As a first step we show that the collection of types with an R-valued relation
(for an arbitrary type R, later taken to be ℝ) to be injective.
We denote this type by Graph' as it generalizes the type Graph of graphs defined
above. Indeed, the injectivity proof mirrors the above construction for Graph.

\begin{code}

open import UF.Subsingletons-Properties

module _ (R : π“₯ Μ‡  ) where

 Graph' : (𝓀 : Universe) β†’ 𝓀 ⁺ βŠ” π“₯ Μ‡
 Graph' 𝓀 = Ξ£ X κž‰ 𝓀 Μ‡  , (X β†’ X β†’ R)

 graph'-structure : 𝓀 Μ‡  β†’ π“₯ βŠ” 𝓀 Μ‡
 graph'-structure X = (X β†’ X β†’ R)

 Graph'-Ξ£-data
  : compatibility-data (graph'-structure {𝓀}) universes-are-flabby-Ξ£
 Graph'-Ξ£-data {𝓀} =
  Ξ£-construction S T T-refl c
   where
    S = graph'-structure

    T : {X Y : 𝓀 Μ‡ } β†’ X ≃ Y β†’ S X β†’ S Y
    T 𝕗 ΞΌ y y' = ΞΌ (⌜ 𝕗 ⌝⁻¹ y) (⌜ 𝕗 ⌝⁻¹ y')

    T-refl : {X : 𝓀 Μ‡ } β†’ T (≃-refl X) ∼ id
    T-refl R = refl

    module _ (p : Ξ© 𝓀) (A : p holds β†’ 𝓀 Μ‡) where

     r :  S (Ξ£ A) β†’ ((h : p holds) β†’ S (A h))
     r ΞΌ h a a' = ΞΌ (h , a) (h , a')

     _ : r ＝ ρΣ S T T-refl p A
     _ = refl

     Οƒ : ((h : p holds) β†’ S (A h)) β†’ S (Ξ£ A)
     Οƒ g (h , a) (h' , a') =
      g h (⌜ Ξ£-π•šπ•Ÿ p {A} h ⌝⁻¹ (h , a)) (⌜ Ξ£-π•šπ•Ÿ p h ⌝⁻¹ (h' , a'))

     rΟƒ : r ∘ Οƒ ∼ id
     rσ g = dfunext fe' (λ h →
            dfunext fe' (Ξ» a β†’
            dfunext fe' (Ξ» a' β†’
            apβ‚‚ (g h) (transport-over-prop (holds-is-prop p))
                      (transport-over-prop (holds-is-prop p)))))

    c : compatibility-data-Ξ£ S T T-refl
    c p A = σ p A , rσ p A

 ainjectivity-of-Graph'
  : ainjective-type (Graph' 𝓀) 𝓀 𝓀
 ainjectivity-of-Graph' =
  ainjectivity-of-type-of-structures
   graph'-structure
   universes-are-flabby-Ξ£
   Graph'-Ξ£-data

\end{code}

We now take R = ℝ, the type of Dedekind reals, and additionally impose the
axioms of a metric space.

This mirrors the above construction for the type of posets.

\begin{code}

open import UF.PropTrunc

module _
        (pt : propositional-truncations-exist)
       where

 open PropositionalTruncation pt

 private
  pe : PropExt
  pe = Univalence-gives-PropExt ua

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

 open import DedekindReals.Addition fe' pe' pt
  renaming (_+_ to _+ℝ_) hiding (_-_)
 open import DedekindReals.Order fe' pe' pt
 open import DedekindReals.Type fe' pe' pt
 open import MetricSpaces.StandardDefinition fe' pe' pt

 Metric-Space-Ξ£-data : compatibility-data {(𝓀 βŠ” 𝓀₁) ⁺}
                        (Ξ» M β†’ Ξ£ d κž‰ (M β†’ M β†’ ℝ) , metric-axioms M d)
                        universes-are-flabby-Ξ£
 Metric-Space-Ξ£-data =
  compatibility-data-with-axioms
   universes-are-flabby-Ξ£
   (graph'-structure ℝ)
   (Graph'-Ξ£-data ℝ)
   metric-axioms
   metric-axioms-is-prop
   axioms-Ξ£-data
  where
   Οƒ : (p : Ξ© 𝓀) (A : p holds β†’ 𝓀 Μ‡ )
     β†’ ((h : p holds) β†’ graph'-structure ℝ (A h))
     β†’ graph'-structure ℝ (Ξ£ A)
   Οƒ p A = section-map
            (ρ (graph'-structure ℝ) universes-are-flabby-Ξ£ p A)
            (Graph'-Ξ£-data ℝ p A)

   axioms-Ξ£-data
    : (p : Ξ© 𝓀)
      (A : p holds β†’ 𝓀 Μ‡ )
      (Ξ± : (h : p holds) β†’ graph'-structure ℝ (A h))
      (F : (h : p holds) β†’ metric-axioms (A h) (Ξ± h))
    β†’ metric-axioms (Ξ£ A) (Οƒ p A Ξ±)
   axioms-Ξ£-data p A Ξ± F = I , II , III
    where
     dβ‚š : {h : p holds} β†’ A h β†’ A h β†’ ℝ
     dβ‚š {h} = Ξ± h

     dβ‚š-reflexive : {h : p holds} β†’ reflexivity (A h) dβ‚š
     dβ‚š-reflexive {h} = pr₁ (F h)

     dβ‚š-symmetric : {h : p holds} β†’ symmetry (A h) dβ‚š
     dβ‚š-symmetric {h} = pr₁ (prβ‚‚ (F h))

     dβ‚š-triangle-inequality : {h : p holds} β†’ triangle-inequality (A h) dβ‚š
     dβ‚š-triangle-inequality {h} = prβ‚‚ (prβ‚‚ (F h))

     i : {h h' : p holds} β†’ h ＝ h'
     i = holds-is-prop p _ _

     Ο„ : {h h' : p holds} β†’ A h β†’ A h'
     Ο„ = transport A i

     d : Ξ£ A β†’ Ξ£ A β†’ ℝ
     d (h₁ , a₁) (hβ‚‚ , aβ‚‚) = Ξ± h₁ (Ο„ a₁) (Ο„ aβ‚‚)

     generalized-lemma : {h₁ hβ‚‚ : p holds} {a₁ : A h₁} {aβ‚‚ : A hβ‚‚}
                         (e₁ : hβ‚‚ ＝ h₁) (eβ‚‚ : h₁ ＝ h₁)
                         (e₃ : hβ‚‚ ＝ hβ‚‚) (eβ‚„ : h₁ ＝ hβ‚‚)
                       β†’ Ξ± h₁ (transport A e₁ aβ‚‚) (transport A eβ‚‚ a₁)
                       ＝ Ξ± hβ‚‚ (transport A e₃ aβ‚‚) (transport A eβ‚„ a₁)
     generalized-lemma {h₁} {hβ‚‚} {a₁} {aβ‚‚} refl eβ‚‚ e₃ eβ‚„ =
      apβ‚‚ (Ξ± hβ‚‚)
          ((transport-over-prop' (holds-is-prop p) e₃) ⁻¹)
          (ap (Ξ» - β†’ transport A - a₁)
              (props-are-sets (holds-is-prop p) eβ‚‚ eβ‚„))

     dβ‚š-equals-d : {h₁ hβ‚‚ : p holds} {a₁ : A h₁} {aβ‚‚ : A hβ‚‚}
                 β†’ dβ‚š (Ο„ a₁) (Ο„ aβ‚‚) ＝ d (h₁ , a₁) (hβ‚‚ , aβ‚‚)
     dβ‚š-equals-d = refl

     dβ‚š-equals-d-left : {h₁ hβ‚‚ : p holds} {a₁ : A h₁} {aβ‚‚ : A hβ‚‚}
                      β†’ dβ‚š (Ο„ a₁) aβ‚‚ ＝ d (h₁ , a₁) (hβ‚‚ , aβ‚‚)
     dβ‚š-equals-d-left = generalized-lemma i refl i i

     dβ‚š-equals-d-right : {h₁ hβ‚‚ : p holds} {a₁ : A h₁} {aβ‚‚ : A hβ‚‚}
                       β†’ dβ‚š a₁ (Ο„ aβ‚‚) ＝ d (h₁ , a₁) (hβ‚‚ , aβ‚‚)
     dβ‚š-equals-d-right = generalized-lemma refl refl i refl

     _ : Οƒ p A Ξ± ＝ d
     _ = refl -- Which is crucial for the proof below to work.

     I : reflexivity (Ξ£ A) (Οƒ p A Ξ±)
     I x@(h₁ , a) y@(hβ‚‚ , a') = I₁ , Iβ‚‚
      where
       I₁ : d x y ＝ 0ℝ β†’ x ＝ y
       I₁ e = to-Ξ£-＝ (i , lr-implication (dβ‚š-reflexive (Ο„ a) a') (dβ‚š-equals-d-left βˆ™ e))
       Iβ‚‚ : x ＝ y β†’ d x y ＝ 0ℝ
       Iβ‚‚ refl = rl-implication (dβ‚š-reflexive (Ο„ a) (Ο„ a)) refl

     II : symmetry (Ξ£ A) d
     II (h₁ , a₁) (hβ‚‚ , aβ‚‚) =
      dβ‚š {h₁} (Ο„ a₁) (Ο„ aβ‚‚) ＝⟨ dβ‚š-symmetric (Ο„ a₁) (Ο„ aβ‚‚) ⟩
      dβ‚š {h₁} (Ο„ aβ‚‚) (Ο„ a₁) ＝⟨ generalized-lemma i i i i ⟩
      dβ‚š {hβ‚‚} (Ο„ aβ‚‚) (Ο„ a₁) ∎

     III : triangle-inequality (Ξ£ A) (Οƒ p A Ξ±)
     III x@(h₁ , a₁) y@(hβ‚‚ , aβ‚‚) z@(h₃ , a₃) = IIIβ‚‚
      where
       III₁ : dβ‚š {hβ‚‚} (Ο„ a₁) aβ‚‚ +ℝ dβ‚š {hβ‚‚} aβ‚‚ (Ο„ a₃) ≀ℝ dβ‚š {hβ‚‚} (Ο„ a₁) (Ο„ a₃)
       III₁ = dβ‚š-triangle-inequality (Ο„ a₁) aβ‚‚ (Ο„ a₃)
       IIIβ‚‚ : d x y +ℝ d y z ≀ℝ d x z
       IIIβ‚‚ = transport₃ (Ξ» r₁ rβ‚‚ r₃ β†’ r₁ +ℝ rβ‚‚ ≀ℝ r₃)
              dβ‚š-equals-d-left dβ‚š-equals-d-right (lem i i) III₁
        where
         lem : (e₁ : h₁ ＝ hβ‚‚) (eβ‚‚ : h₃ ＝ hβ‚‚)
             β†’ dβ‚š {hβ‚‚} (transport A e₁ a₁) (transport A eβ‚‚ a₃)
               ＝ d (h₁ , a₁) (h₃ , a₃)
         lem refl refl = generalized-lemma refl refl i i

 ainjectivity-of-Metric-Space
  : ainjective-type (Metric-Space (𝓀₁ βŠ” 𝓀)) (𝓀₁ βŠ” 𝓀) (𝓀₁ βŠ” 𝓀)
 ainjectivity-of-Metric-Space {𝓀} =
  ainjectivity-of-type-of-structures
   (Ξ» M β†’ Ξ£ d κž‰ (M β†’ M β†’ ℝ) , metric-axioms M d)
   universes-are-flabby-Ξ£
   (Metric-Space-Ξ£-data {𝓀})

\end{code}