Marc Bezem, Thierry Coquand, Peter Dybjer, Martin Escardo
18th March 2025.

Discussion about whether a certain transport can be performed more
easily using univalence than "by hand". In particular, does
cumulativity help?

This discussion is inconclusive for the moment.

\begin{code}

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

module gist.transport-discussion where

open import MLTT.Spartan
open import UF.Equiv
open import UF.FunExt
open import UF.Subsingletons
open import UF.Univalence
open import UF.UniverseEmbedding
open import Ordinals.Type
open import Ordinals.Underlying
open import Ordinals.Equivalence

\end{code}

The following transport is performed by hand in the following imported
module.

\begin{code}

module _ (fe : FunExt) where

 open import Ordinals.WellOrderTransport fe

 _ : (X : 𝓀 Μ‡ ) (Ξ± : Ordinal π“₯)
   β†’ X ≃ ⟨ Ξ± ⟩
   β†’ resizable-order Ξ± 𝓀
   β†’ Ξ£ s κž‰ OrdinalStructure X , (X , s) ≃ₒ Ξ±
 _ = transfer-structure

\end{code}

Can it be done, instead, using univalence in the absence of
cumulativity? If not, would cumulativity help?

We consider a simplified version of the problem to reduce labour. We
could even remove the requirement that there is at most one edge
between any two vertices, but this is useful to prove a no-go theorem
below. We could also require that the type V of vertices is a set, but
we try to keep things as simple as possible.

\begin{code}

reflexive-structure : (𝓦 : Universe) β†’ 𝓣 Μ‡  β†’ 𝓦 ⁺ βŠ” 𝓣 Μ‡
reflexive-structure 𝓦 V = Ξ£ _β‡’_ κž‰ (V β†’ V β†’ 𝓦 Μ‡)
                                 , ((v : V) β†’ v β‡’ v)
                                 Γ— ((v v' : V) β†’ is-prop (v β‡’ v'))

Reflexive-Graph : (𝓦 𝓣 : Universe) β†’ (𝓦 βŠ” 𝓣)⁺ Μ‡
Reflexive-Graph 𝓦 𝓣 = Ξ£ V κž‰ 𝓣 Μ‡ , reflexive-structure 𝓦 V

\end{code}

We now formulate the notion of reflexive graph equivalence, for the
above notion of reflexive graph. Using SIP, and assuming univalence,
we can show that for graphs in the same universes, identity is
canonically equivalent to this notion of reflexive graph
equivalence. But we won't bother to prove this, at least not for the
moment.

\begin{code}

_≃ʳᡍ_ : {𝓦 𝓣 𝓦' 𝓣' : Universe}
      β†’ Reflexive-Graph 𝓦 𝓣 β†’ Reflexive-Graph 𝓦' 𝓣' β†’ 𝓦 βŠ” 𝓣 βŠ” 𝓦' βŠ” 𝓣' Μ‡
(V , _β‡’_ , _) ≃ʳᡍ (V' , _β‡’'_ , _)
 = Ξ£ f κž‰ (V ≃ V'), ((vβ‚€ v₁ : V') β†’ (⌜ f ⌝⁻¹ vβ‚€ β‡’ ⌜ f ⌝⁻¹ v₁) ≃ (vβ‚€ β‡’' v₁))

\end{code}

So here is our experimental discussion.

\begin{code}

module discussion
        (𝓀 π“₯ : Universe)
        (𝓐@(A , _β‡’_ , β‡’-refl , β‡’-is-prop-valued) : Reflexive-Graph π“₯ π“₯)
        (_β‡’'_ : A β†’ A β†’ 𝓀 Μ‡ )
        (resizing-assumption : (a b : A) β†’ (a β‡’ b) ≃ (a β‡’' b))
        (X : 𝓀 Μ‡ )
        (f : X ≃ A)
        (ua : is-univalent (𝓀 βŠ” π“₯))
        (sorry : {𝓦 : Universe} {S : 𝓦 Μ‡} β†’ S)
      where

\end{code}

We don't have cumulativity, so we lift explicitly.

\begin{code}

 X⁺ A⁺ : 𝓀 βŠ” π“₯ Μ‡
 X⁺ = Lift (𝓀 βŠ” π“₯) X
 A⁺ = Lift (𝓀 βŠ” π“₯) A

 II : X⁺ ≃ A⁺
 II = X⁺ β‰ƒβŸ¨ Lift-≃ (𝓀 βŠ” π“₯) X ⟩
      X  β‰ƒβŸ¨ f ⟩
      A  β‰ƒβŸ¨ ≃-Lift (𝓀 βŠ” π“₯) A ⟩
      A⁺ β– 

\end{code}

The following apologies can be filled by transporting by hand as in
the function `transfer-structure` mentioned above.

Presumably they don't need proof in a universe-cumulative system,
where X⁺ and A⁺ are simply X and A, so that we have false apologies.

\begin{code}

 _⇒⁺_ : A⁺ β†’ A⁺ β†’ π“₯ Μ‡
 a ⇒⁺ b = sorry

 ⇒⁺-refl : (a : A⁺) β†’ a ⇒⁺ a
 ⇒⁺-refl = sorry

 ⇒⁺-is-prop-valued : (a b : A⁺) β†’ is-prop (a ⇒⁺ b)
 ⇒⁺-is-prop-valued = sorry

 rsₐ : reflexive-structure π“₯ A⁺
 rsₐ = _⇒⁺_ , ⇒⁺-refl , ⇒⁺-is-prop-valued

 I : X⁺ ＝ A⁺
 I = eqtoid ua (X⁺) (A⁺) II

 rsβ‚“ : reflexive-structure π“₯ X⁺
 rsβ‚“ = transport⁻¹ (reflexive-structure π“₯) I rsₐ

\end{code}

But there is limit to the number of false apologies one can make.

The following needs more than cumulativity. And this is why we have
the above assumptions `_β‡’'_` and `resizing-assumption` (which
correspond to the `resizable-order` condition in `transfer-structure`).
Without them, we get a no-go theorem (see `resizing-taboo` below).

So the following are genuine apologies: They can't just hold on the
nose by cumulativity.

\begin{code}

 _β‡’β‚“_ : X β†’ X β†’ 𝓀 Μ‡
 _β‡’β‚“_ = sorry

 β‡’β‚“-refl : (x : X) β†’ x β‡’β‚“ x
 β‡’β‚“-refl = sorry

 β‡’β‚“-is-prop-valued : (x y : X) β†’ is-prop (x β‡’β‚“ y)
 β‡’β‚“-is-prop-valued = sorry

 𝓧 : Reflexive-Graph 𝓀 𝓀
 𝓧 = X , _β‡’β‚“_ , β‡’β‚“-refl , β‡’β‚“-is-prop-valued

 transfer-structure-analogue : 𝓧 ≃ʳᡍ 𝓐
 transfer-structure-analogue = sorry

\end{code}

Of course all the apologies can be removed, even without cumulativity,
by following the strategy of `transfer-structure` by transporting
structure and properties by hand, without univalence.

The question here is whether univalence, perhaps with the help of
cumulativity, can avoid transport by hand.

We now formulate and prove the no-go theorem. Because it holds in the
absence of cumulativity, it also holds in its presence.

The following type is a distilled version of the type of the function
`transfer-structure`, but without the `resizable-order` assumption.

\begin{code}

Transport-Assumption : 𝓀ω
Transport-Assumption =
   {𝓀 π“₯ : Universe} (X : 𝓀 Μ‡ ) (A : π“₯ Μ‡ )
   (f : X ≃ A)
   (rsₐ : reflexive-structure π“₯ A)
 β†’ Ξ£ rsβ‚“ κž‰ reflexive-structure 𝓀 X , (X , rsβ‚“) ≃ʳᡍ (A , rsₐ)

open import UF.Size
open import UF.EquivalenceExamples

resizing-taboo : Transport-Assumption β†’ Propositional-Resizing
resizing-taboo t {π“₯} {𝓀} = Ξ³
 where
  module _ (P : π“₯ Μ‡) (P-is-prop : is-prop P) where
   X : 𝓀 Μ‡
   X = πŸ™ {𝓀} + πŸ™ {𝓀}

   A : π“₯ Μ‡
   A = πŸ™ {π“₯} + πŸ™ {π“₯}

   I : X ≃ A
   I = +-cong one-πŸ™-only one-πŸ™-only

   _β‡’_ : A β†’ A β†’ π“₯ Μ‡
   inl ⋆ β‡’ inl ⋆ = πŸ™
   inl ⋆ β‡’ inr ⋆ = πŸ™ -- It's not important what we choose in this case.
   inr ⋆ β‡’ inl ⋆ = P
   inr ⋆ β‡’ inr ⋆ = πŸ™

   β‡’-refl : (a : A) β†’ a β‡’ a
   β‡’-refl (inl ⋆) = ⋆
   β‡’-refl (inr ⋆) = ⋆

   β‡’-is-prop-valued : (a b : A) β†’ is-prop (a β‡’ b)
   β‡’-is-prop-valued (inl ⋆) (inl ⋆) = πŸ™-is-prop
   β‡’-is-prop-valued (inl ⋆) (inr ⋆) = πŸ™-is-prop
   β‡’-is-prop-valued (inr ⋆) (inl ⋆) = P-is-prop
   β‡’-is-prop-valued (inr ⋆) (inr ⋆) = πŸ™-is-prop

   rₐ : reflexive-structure π“₯ A
   rₐ = (_β‡’_ , β‡’-refl , β‡’-is-prop-valued)

   II : Ξ£ rβ‚“ κž‰ reflexive-structure 𝓀 X , (X , rβ‚“) ≃ʳᡍ (A , rₐ)
   II = t X A I rₐ

   III : type-of II β†’ P is 𝓀 small
   III ((_β‡’β‚“_ , β‡’β‚“-refl , β‡’β‚“-is-prop-valued) , f , g) =
    Pβ‚“ , IV
    where
     Pβ‚“ : 𝓀 Μ‡
     Pβ‚“ = ⌜ f ⌝⁻¹ (inr ⋆) β‡’β‚“ ⌜ f ⌝⁻¹ (inl ⋆)

     Pβ‚“-is-prop : is-prop Pβ‚“
     Pβ‚“-is-prop = β‡’β‚“-is-prop-valued (⌜ f ⌝⁻¹ (inr ⋆)) (⌜ f ⌝⁻¹ (inl ⋆))

     IV : Pβ‚“ ≃ P
     IV = g (inr ⋆) (inl ⋆)

   Ξ³ : P is 𝓀 small
   Ξ³ = III II

\end{code}

NB. If we wanted to prove the converse, we would still have to chase
equivalences by hand, as far as we know at the time of writing, unless
we have propositional resizing on-the-nose like UniMath. But notice
that propositional resizing on-the-nose is not unknown to be
consistent.

In other words, there are propositional resizing *axioms* (which are
known to be consistent, and in the above no-go theorem we have a
propositional resizing axiom) and there are propositional resizing
*rules* for the type theory (which are not known to be consistent).

If we hadn't assumed that the edge relation of a reflexive graph is a
proposition, we would instead be able to show that every type in any
universe is equivalent to any type in any universe we wish, which is
of course false, as "there are more types in larger universes".