Martin Escardo & Tom de Jong, June 2023.

Iterative sets.

We define the type of iterative sets as a subtype of that of multisets.

  * H. R. Gylterud, "From multisets to sets in homotopy type theory".
    The Journal of Symbolic Logic, vol. 83, no. 3, pp. 1132–1146,
    2018. https://doi.org/10.1017/jsl.2017.84

See the module Iterative.index for further bibliographic references.

The previous module Iterative.Multisets doesn't make significant use
of univalence, and so we assumed it only for specific
constructions. But here the use of univalence is more pervasive, and
so we assume it globally.

\begin{code}

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

open import MLTT.Spartan
open import UF.Univalence

module Iterative.Sets
        (ua : Univalence)
        (𝓀 : Universe)
       where

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

private
 𝓀⁺ : Universe
 𝓀⁺ = 𝓀 ⁺

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

 fe' : FunExt
 fe' 𝓀 π“₯ = fe {𝓀} {π“₯}

open import Iterative.Multisets 𝓀
open import Ordinals.Notions
open import UF.Base
open import UF.DiscreteAndSeparated
open import UF.Embeddings
open import UF.Equiv
open import UF.EquivalenceExamples
open import UF.PairFun
open import UF.Retracts
open import UF.Sets
open import UF.Size
open import UF.Subsingletons
open import UF.Subsingletons-FunExt
open import W.Type

\end{code}

An iterative set is a multiset whose subforests are all
embeddings. The effect of that is that the membership relation on
iterative sets is proposition-valued, rather than just type-valued, as
is the case for general multisets.

\begin{code}

is-iterative-set : 𝕄 β†’ 𝓀⁺ Μ‡
is-iterative-set (ssup X Ο†) = is-embedding Ο†
                            Γ— ((x : X) β†’ is-iterative-set (Ο† x))
\end{code}

It is convenient to name the projections for the sake of clarity:

\begin{code}

𝕄-forest-is-embedding : (M : 𝕄)
                      β†’ is-iterative-set M
                      β†’ is-embedding (𝕄-forest M)
𝕄-forest-is-embedding (ssup _ _) = pr₁

𝕄-subtrees-are-iterative : (M : 𝕄)
                         β†’ is-iterative-set M
                         β†’ (x : 𝕄-root M) β†’ is-iterative-set (𝕄-forest M x)
𝕄-subtrees-are-iterative (ssup _ _) = prβ‚‚

\end{code}

It is crucial that the notion of iterative set is property rather than
data:

\begin{code}

being-iset-is-prop : (M : 𝕄) β†’ is-prop (is-iterative-set M)
being-iset-is-prop (ssup X Ο†) =
 Γ—-is-prop
  (being-embedding-is-prop fe Ο†)
  (Ξ -is-prop fe (Ξ» x β†’ being-iset-is-prop (Ο† x)))

\end{code}

The type of iterative sets as a subtype of that of iterative
multisets:

\begin{code}

𝕍 : 𝓀⁺ Μ‡
𝕍 = Ξ£ M κž‰ 𝕄 , is-iterative-set M

𝕍-is-locally-small : is-locally-small 𝕍
𝕍-is-locally-small = subtype-is-locally-small
                      being-iset-is-prop
                      (𝕄-is-locally-small ua)
\end{code}

We again name the projections for the sake of clarity:

\begin{code}

underlying-mset : 𝕍 β†’ 𝕄
underlying-mset = pr₁

isets-are-iterative : (A : 𝕍) β†’ is-iterative-set (underlying-mset A)
isets-are-iterative = prβ‚‚

\end{code}

Because the notion of iterative set is property, we get that 𝕍 is
indeed a subtype of 𝕄.

\begin{code}

underlying-mset-is-embedding : is-embedding underlying-mset
underlying-mset-is-embedding = pr₁-is-embedding being-iset-is-prop

\end{code}

We define the root and the forest of an iterative set in terms of
those for multisets, but we need to add a "proof obligation" in the
case of the forest.

\begin{code}

𝕍-root : 𝕍 β†’ 𝓀 Μ‡
𝕍-root A = 𝕄-root (underlying-mset A)

𝕍-forest : (A : 𝕍) β†’ 𝕍-root A β†’ 𝕍
𝕍-forest A x = 𝕄-forest (underlying-mset A) x ,
               𝕄-subtrees-are-iterative
                (underlying-mset A)
                (isets-are-iterative A)
                x

\end{code}

A criterion for equality in 𝕍:

\begin{code}

to-𝕍-＝ : {X Y : 𝓀 Μ‡ }
          {Ο† : X β†’ 𝕄}
          {Ξ³ : Y β†’ 𝕄}
        β†’ (Ξ£ p κž‰ X ＝ Y , Ο† ＝ Ξ³ ∘ Idtofun p)
        β†’ (i : is-iterative-set (ssup X Ο†))
          (j : is-iterative-set (ssup Y Ξ³))
        β†’ (ssup X Ο† , i) ＝[ 𝕍 ] (ssup Y Ξ³ , j)
to-𝕍-＝ Οƒ i j = to-subtype-＝ being-iset-is-prop (to-𝕄-＝ Οƒ)

\end{code}

We define membership of iterative sets in terms of that for multisets:

\begin{code}

_∈_ : 𝕍 β†’ 𝕍 β†’ 𝓀⁺ Μ‡
A ∈ B = underlying-mset A ⁅ underlying-mset B

\end{code}

As is the case for iterative multisets, there is a resized down,
equivalent definition of membership.

\begin{code}

_∈⁻_ : 𝕍 β†’ 𝕍 β†’ 𝓀 Μ‡
A ∈⁻ B = underlying-mset A ⁅⁻ underlying-mset B

βˆˆβ»β‰ƒβˆˆ : (A B : 𝕍) β†’ (A ∈ B) ≃ (A ∈⁻ B)
βˆˆβ»β‰ƒβˆˆ A B = ⁅⁻≃⁅ ua (underlying-mset A) (underlying-mset B)

\end{code}

As discussed above, the membership relation becomes a proposition
precisely because we required forests to be embeddings to define the
subtype of iterative sets.

\begin{code}

∈-is-prop-valued : (A B : 𝕍) β†’ is-prop (A ∈ B)
∈-is-prop-valued (M , _) (ssup X Ο† , Ο†-emb , _) = Ο†-emb M

𝕍-forest-∈ : (A : 𝕍) (x : 𝕍-root A) β†’ 𝕍-forest A x ∈ A
𝕍-forest-∈ A x = 𝕄-forest-⁅ (underlying-mset A) x

\end{code}

The subset relation is defined in the usual way and is
proposition-valued:

\begin{code}

_βŠ†_ : 𝕍 β†’ 𝕍 β†’ 𝓀⁺ Μ‡
A βŠ† B = (C : 𝕍) β†’ C ∈ A β†’ C ∈ B

βŠ†-is-prop-valued : (A B : 𝕍) β†’ is-prop (A βŠ† B)
βŠ†-is-prop-valued A B = Ξ β‚‚-is-prop fe (Ξ» C _ β†’ ∈-is-prop-valued C B)

\end{code}

It is in the following that the univalence axiom is used for the first
time, to establish the extensionality axiom for iterative sets:

\begin{code}

∈-is-extensional : (A B : 𝕍) β†’ A βŠ† B β†’ B βŠ† A β†’ A ＝ B
∈-is-extensional A@(M@(ssup X Ο†) , Ο†-emb , g)
                 B@(N@(ssup Y Ξ³) , Ξ³-emb , h) u v = V
 where
  have-uv : (A βŠ† B) Γ— (B βŠ† A)
  have-uv = u , v

  I : (x : X) β†’ Ξ£ y κž‰ Y , Ξ³ y ＝ Ο† x
  I x = u (Ο† x , g x) (𝕄-forest-⁅ M x)

  II : (y : Y) β†’ Ξ£ x κž‰ X , Ο† x ＝ Ξ³ y
  II y = v (Ξ³ y , h y) (𝕄-forest-⁅ N y)

  f : X β†’ Y
  f x = pr₁ (I x)

  f⁻¹ : Y β†’ X
  f⁻¹ y = pr₁ (II y)

  η : f⁻¹ ∘ f ∼ id
  Ξ· x = embeddings-are-lc Ο† Ο†-emb
         (Ο† (f⁻¹ (f x)) ＝⟨ prβ‚‚ (II (f x)) ⟩
          Ξ³ (f x)       ＝⟨ prβ‚‚ (I x) ⟩
          Ο† x           ∎)

  Ρ : f ∘ f⁻¹ ∼ id
  Ξ΅ y = embeddings-are-lc Ξ³ Ξ³-emb
         (Ξ³ (f (f⁻¹ y)) ＝⟨ prβ‚‚ (I (f⁻¹ y)) ⟩
          Ο† (f⁻¹ y)     ＝⟨ prβ‚‚ (II y) ⟩
          γ y           ∎)

  𝕗 : X ≃ Y
  𝕗 = qinveq f (f⁻¹ , Ξ· , Ξ΅)

  p : X ＝ Y
  p = eqtoid (ua 𝓀) X Y 𝕗

  III : Idtofun p ＝ f
  III = Idtofun-eqtoid (ua 𝓀) 𝕗

  IV = Ξ» x β†’
   Ο† x             ＝⟨ (prβ‚‚ (I x))⁻¹ ⟩
   Ξ³ (f x)         ＝⟨ ap (Ξ» - β†’ Ξ³ (- x)) (III ⁻¹) ⟩
   γ (Idtofun p x) ∎

  V : A ＝ B
  V = to-𝕍-＝ (p , dfunext fe IV) (Ο†-emb , g) (Ξ³-emb , h)

\end{code}

It follows that 𝕍 is 0-type, or set, in the sense of the HoTT
book. But notice that we now have two notions of set in this
discussion: the "material" (iterative set) one and the "structural"
one (0-type or set). The reader should keep this distinction in mind
for the comments and code below.

The following uses the fact that any type with an extensional order is
automatically a set.

\begin{code}

𝕍-is-set : is-set 𝕍
𝕍-is-set = extensionally-ordered-types-are-sets _∈_ fe'
            ∈-is-prop-valued
            ∈-is-extensional

\end{code}

Here is a second, more direct, proof of this fact.

The following says that ssup Ο† ＝ M is a proposition for every M : 𝕄
if Ο† is an embedding.

The following doesn't seem to have been observed before in the
literature.

\begin{code}

𝕄-ssup-is-h-isolated : (X : 𝓀 Μ‡ ) (Ο† : X β†’ 𝕄)
                     β†’ is-embedding Ο†
                     β†’ is-h-isolated (ssup X Ο†)
𝕄-ssup-is-h-isolated X Ο† Ο†-emb {M} = III
 where
  I = (ssup X Ο† ＝ M)                        β‰ƒβŸ¨ ＝-flip ⟩
      (M ＝ ssup X Ο†)                        β‰ƒβŸ¨ 𝕄-＝' M (ssup X Ο†) ⟩
      fiber ((Ο† ∘_) ∘ Idtofun) (𝕄-forest M)  β– 

  II : is-embedding ((Ο† ∘_) ∘ Idtofun)
  II = ∘-is-embedding
        (Idtofun-is-embedding (ua 𝓀) fe)
        (postcomp-is-embedding fe' Ο† Ο†-emb)

  III : is-prop (ssup X Ο† ＝ M)
  III = equiv-to-prop I (II (𝕄-forest M))

\end{code}

And a particular case of this is that if M is an iterative set then
M ＝ N is a proposition for every *multiset* N.

\begin{code}

isets-are-h-isolated : (M : 𝕄)
                     β†’ is-iterative-set M
                     β†’ is-h-isolated M
isets-are-h-isolated (ssup X Ο†) (Ο†-emb , _) = 𝕄-ssup-is-h-isolated X Ο† Ο†-emb

\end{code}

Because a subtype of any type whatsoever consisting of h-isolated
elements is a 0-type, we get a second proof that the type of iterative
sets is a 0-type.

\begin{code}

𝕍-is-set' : is-set 𝕍
𝕍-is-set' {M , M-is-is-set} =
 equiv-to-prop
  (≃-sym (to-subtype-＝-≃ being-iset-is-prop))
  (isets-are-h-isolated M M-is-is-set)

\end{code}

By definition, an iterative multiset is an iterative set if its
𝕄-forests are all embeddings. The 𝕍-forests are also embeddings:

\begin{code}

𝕍-forest-is-embedding : (A : 𝕍) β†’ is-embedding (𝕍-forest A)
𝕍-forest-is-embedding A@(ssup X Ο† , Ο†-emb , Ο†-iter) =
 pair-fun-is-embedding-special Ο† Ο†-iter Ο†-emb being-iset-is-prop

\end{code}

We construct elements of 𝕄 using the constructor ssup. We now
introduce a corresponding constructor 𝕍-ssup to construct elements of
the type 𝕍.

\begin{code}

𝕍-ssup : (X : 𝓀 Μ‡ ) (Ο• : X β†’ 𝕍) β†’ is-embedding Ο• β†’ 𝕍
𝕍-ssup X Ο• Ο•-emb = ssup X Ο† , Ο†-emb , Ο†-iset
 where
  Ο† : X β†’ 𝕄
  Ο† = underlying-mset ∘ Ο•

  Ο†-iset : (x : X) β†’ is-iterative-set (Ο† x)
  Ο†-iset = isets-are-iterative ∘ Ο•

  Ο†-emb : is-embedding Ο†
  Ο†-emb = ∘-is-embedding Ο•-emb underlying-mset-is-embedding

\end{code}

It behaves as expected with respect to the corresponding destructors:

\begin{code}

𝕍-ssup-root : (X : 𝓀 Μ‡ ) (Ο• : X β†’ 𝕍) (e : is-embedding Ο•)
            β†’ 𝕍-root (𝕍-ssup X Ο• e) ＝ X
𝕍-ssup-root X Ο• e = refl

𝕍-ssup-forest : (X : 𝓀 Μ‡ ) (Ο• : X β†’ 𝕍) (e : is-embedding Ο•)
              β†’ 𝕍-forest (𝕍-ssup X Ο• e) ＝ Ο•
𝕍-ssup-forest X Ο• e = refl

\end{code}

Notice that the identifications are definitional.

We have the following Ξ· rules for 𝕍, where the first is more general
and the second is more natural. In both cases the identifications are
not definitional.

\begin{code}

𝕍-Ξ·' : (A : 𝕍) (e : is-embedding (𝕍-forest A))
     β†’ 𝕍-ssup (𝕍-root A) (𝕍-forest A) e ＝ A
𝕍-Ξ·' (ssup _ _ , _) _ = to-subtype-＝ being-iset-is-prop refl

𝕍-Ξ· : (A : 𝕍) β†’ 𝕍-ssup (𝕍-root A) (𝕍-forest A) (𝕍-forest-is-embedding A) ＝ A
𝕍-Ξ· A = 𝕍-Ξ·' A (𝕍-forest-is-embedding A)

\end{code}

Here are two characterizations of the membership relation:

\begin{code}

∈-behaviour : (A : 𝕍) (X : 𝓀 Μ‡ ) (Ο• : X β†’ 𝕍) (e : is-embedding Ο•)
            β†’ A ∈ 𝕍-ssup X Ο• e ≃ (Ξ£ x κž‰ X , Ο• x ＝ A)
∈-behaviour A X Ο• e =
 (A ∈ 𝕍-ssup X Ο• e)                                     β‰ƒβŸ¨by-definition⟩
 (Ξ£ x κž‰ X , underlying-mset (Ο• x) ＝ underlying-mset A) β‰ƒβŸ¨ Ξ£-cong I ⟩
 (Ξ£ x κž‰ X , Ο• x ＝ A)                                   β– 
  where
   I : (x : X) β†’ (underlying-mset (Ο• x) ＝ underlying-mset A) ≃ (Ο• x ＝ A)
   I x = embedding-criterion-converse
          underlying-mset
          underlying-mset-is-embedding
          (Ο• x)
          A

∈-behaviour' : (A B : 𝕍) β†’ A ∈ B ≃ (Ξ£ x κž‰ 𝕍-root B , 𝕍-forest B x ＝ A)
∈-behaviour' A B =
 transport
  (Ξ» - β†’ A ∈ - ≃ (Ξ£ x κž‰ 𝕍-root - , 𝕍-forest - x ＝ A))
  (𝕍-Ξ· B)
  (∈-behaviour A (𝕍-root B) (𝕍-forest B) (𝕍-forest-is-embedding B))

private
 ∈-remark : (A B : 𝕍) β†’ A ∈ B ≃ fiber (𝕍-forest B) A
 ∈-remark = ∈-behaviour'

\end{code}

It also follows from the facts that 𝕍 is a set and that 𝕍-forest is an
embedding that the root of any iterative set is a 0-type:

\begin{code}

𝕍-root-is-set : (A : 𝕍) β†’ is-set (𝕍-root A)
𝕍-root-is-set A = subtypes-of-sets-are-sets
                   (𝕍-forest A)
                   (𝕍-forest-is-embedding A)
                   𝕍-is-set
\end{code}

It would be nice if we could define 𝕍 inductively as follows:

 data 𝕍 : 𝓀⁺ Μ‡ where
  𝕍-ssup : (X : 𝓀 Μ‡ ) (Ο† : X β†’ 𝕍) β†’ is-embedding Ο† β†’ 𝕍

However, this is not a strictly positive definition, for the criterion
of strict positivity adopted by Agda, and so it is not accepted.

Nevertheless, all iterative sets *are* generated by the "constructor"
𝕍-ssup, in the following sense, so that we can view 𝕍 as really
inductively defined by the above data declaration.

The following result, implementing the above idea, seems to be new.

\begin{code}

𝕍-Induction'
 : (P : 𝕍 β†’ π“₯ Μ‡ )
   (f : (A : 𝕍) β†’ ((x : 𝕍-root A) β†’ P (𝕍-forest A x)) β†’ P A)
 β†’ Ξ£ h κž‰ ((A : 𝕍) β†’ P A)
       , ((A : 𝕍) β†’ h A ＝ f A (Ξ» x β†’ h (𝕍-forest A x)))
𝕍-Induction' P f = (Ξ» (M , i) β†’ H M i) , p
 where
  H : (M : 𝕄) (i : is-iterative-set M) β†’ P (M , i)
  H M@(ssup X Ο†) i@(_ , Ο†-iter) = f (M , i) (Ξ» x β†’ H (Ο† x) (Ο†-iter x))

  p : (A : 𝕍) β†’ _ ＝ _
  p (M@(ssup X Ο†) , i@(_ , Ο†-iter)) = refl

𝕍-Induction
 : (P : 𝕍 β†’ π“₯ Μ‡ )
 β†’ (f : (X : 𝓀 Μ‡ ) (Ο• : X β†’ 𝕍) (e : is-embedding Ο•)
      β†’ ((x : X) β†’ P (Ο• x))
      β†’ P (𝕍-ssup X Ο• e))
 β†’ Ξ£ h κž‰ ((A : 𝕍) β†’ P A)
       , ((X : 𝓀 Μ‡ ) (Ο• : X β†’ 𝕍) (e : is-embedding Ο•)
       β†’ h (𝕍-ssup X Ο• e) ＝ f X Ο• e (Ξ» x β†’ h (Ο• x)))
𝕍-Induction {π“₯} P f = h , IV
 where
  f' : (A : 𝕍) β†’ ((x : 𝕍-root A) β†’ P (𝕍-forest A x)) β†’ P A
  f' A@(M@(ssup X Ο†) , i@(Ο†-emb , Ο†-iter)) g = II
   where
    I : P (𝕍-ssup X (𝕍-forest A) (𝕍-forest-is-embedding A))
    I = f X (𝕍-forest A) (𝕍-forest-is-embedding A) g

    II : P A
    II = transport P (𝕍-Ξ· A) I

  h : (A : 𝕍) β†’ P A
  h = pr₁ (𝕍-Induction' P f')

  III : (A : 𝕍) β†’ h A ＝ f' A (Ξ» x β†’ h (𝕍-forest A x))
  III = prβ‚‚ (𝕍-Induction' P f')

  IV : (X : 𝓀 Μ‡ ) (Ο• : X β†’ 𝕍) (e : is-embedding Ο•)
     β†’ h (𝕍-ssup X Ο• e) ＝ f X Ο• e (Ξ» x β†’ h (Ο• x))
  IV X Ο• e =
   h A                                                               ＝⟨ III A ⟩
   f' A (Ξ» x β†’ h (Ο• x))                                              ＝⟨refl⟩
   t P                (𝕍-Ξ· A)             (f X Ο• e' (Ξ» x β†’ h (Ο• x))) ＝⟨ i ⟩
   t P                (ap (𝕍-ssup X Ο•) p) (f X Ο• e' (Ξ» x β†’ h (Ο• x))) ＝⟨ ii ⟩
   t (P ∘ 𝕍-ssup X Ο•) p                   (f X Ο• e' (Ξ» x β†’ h (Ο• x))) ＝⟨ iii ⟩
   f X Ο• e (Ξ» x β†’ h (Ο• x))                                           ∎
    where
     t = transport
     A  = 𝕍-ssup X Ο• e
     e' = 𝕍-forest-is-embedding A

     p : e' ＝ e
     p = being-embedding-is-prop fe Ο• e' e

     q : 𝕍-Ξ· A ＝ ap (𝕍-ssup X Ο•) p
     q = 𝕍-is-set _ _

     i   = ap (Ξ» - β†’ t P - (f X Ο• e' (Ξ» x β†’ h (Ο• x)))) q
     ii  = (transport-ap P (𝕍-ssup X Ο•) p)⁻¹
     iii = apd (Ξ» - β†’ f X Ο• - (Ξ» x β†’ h (Ο• x))) p

𝕍-induction : (P : 𝕍 β†’ π“₯ Μ‡ )
            β†’ ((X : 𝓀 Μ‡ ) (Ο• : X β†’ 𝕍) (e : is-embedding Ο•)
                  β†’ ((x : X) β†’ P (Ο• x))
                  β†’ P (𝕍-ssup X Ο• e))
            β†’ (A : 𝕍) β†’ P A
𝕍-induction P f = pr₁ (𝕍-Induction P f)

𝕍-induction-behaviour
 : (P : 𝕍 β†’ π“₯ Μ‡ )
 β†’ (f : (X : 𝓀 Μ‡ ) (Ο• : X β†’ 𝕍) (e : is-embedding Ο•)
      β†’ ((x : X) β†’ P (Ο• x))
      β†’ P (𝕍-ssup X Ο• e))
 β†’ (X : 𝓀 Μ‡ ) (Ο• : X β†’ 𝕍) (e : is-embedding Ο•)
 β†’ 𝕍-induction P f (𝕍-ssup X Ο• e) ＝ f X Ο• e (Ξ» x β†’ 𝕍-induction P f (Ο• x))
𝕍-induction-behaviour P f = prβ‚‚ (𝕍-Induction P f)

𝕍-recursion : (P : π“₯ Μ‡ )
            β†’ ((X : 𝓀 Μ‡ ) (Ο• : X β†’ 𝕍)
                  β†’ is-embedding Ο•
                  β†’ (X β†’ P)
                  β†’ P)
            β†’ 𝕍 β†’ P
𝕍-recursion P = 𝕍-induction (Ξ» _ β†’ P)

𝕍-recursion-behaviour
 : (P : π“₯ Μ‡ )
 β†’ (f : (X : 𝓀 Μ‡ ) (Ο• : X β†’ 𝕍) (e : is-embedding Ο•)
      β†’ (X β†’ P)
      β†’ P)
 β†’ (X : 𝓀 Μ‡ ) (Ο• : X β†’ 𝕍) (e : is-embedding Ο•)
 β†’ 𝕍-recursion P f (𝕍-ssup X Ο• e) ＝ f X Ο• e (Ξ» x β†’ 𝕍-recursion P f (Ο• x))
𝕍-recursion-behaviour P = 𝕍-induction-behaviour (Ξ» _ β†’ P)

𝕍-iteration : (P : π“₯ Μ‡ )
            β†’ ((X : 𝓀 Μ‡ ) β†’ (X β†’ P) β†’ P)
            β†’ 𝕍 β†’ P
𝕍-iteration P f = 𝕍-recursion P (Ξ» X Ο• e β†’ f X)

𝕍-iteration-behaviour
 : (P : π“₯ Μ‡ )
 β†’ (f : (X : 𝓀 Μ‡ ) β†’ (X β†’ P) β†’ P)
 β†’ (X : 𝓀 Μ‡ ) (Ο• : X β†’ 𝕍) (e : is-embedding Ο•)
 β†’ 𝕍-iteration P f (𝕍-ssup X Ο• e) ＝ f X (Ξ» x β†’ 𝕍-iteration P f (Ο• x))
𝕍-iteration-behaviour P f = 𝕍-recursion-behaviour P (Ξ» X Ο• e β†’ f X)

\end{code}

So we are essentially working with (an encoding) of the above
non-strictly positive data type.

The usual induction principle for iterative sets follows directly from
the above form of induction. This consequence is already in Gylterud [4].

\begin{code}

∈-induction : (P : 𝕍 β†’ π“₯ Μ‡ )
            β†’ ((A : 𝕍) β†’ ((B : 𝕍) β†’ B ∈ A β†’ P B) β†’ P A)
            β†’ (A : 𝕍) β†’ P A
∈-induction P IH = 𝕍-induction P f
 where
  f : (X : 𝓀 Μ‡ ) (Ο• : X β†’ 𝕍) (e : is-embedding Ο•)
    β†’ ((x : X) β†’ P (Ο• x))
    β†’ P (𝕍-ssup X Ο• e)
  f X Ο• e IH' = IH A s
   where
    A : 𝕍
    A = 𝕍-ssup X Ο• e

    s : (B : 𝕍) β†’ B ∈ A β†’ P B
    s B@(.(underlying-mset (Ο• x)) , j) (x , refl) = II
     where
      I : P (Ο• x)
      I = IH' x

      II : P (underlying-mset (Ο• x) , j)
      II = transport P (to-subtype-＝ being-iset-is-prop refl) I

\end{code}

And then it follows immediately that the membership relation is
accessible:

\begin{code}

∈-is-accessible : (A : 𝕍) β†’ is-accessible _∈_ A
∈-is-accessible = ∈-induction (is-accessible _∈_) (Ξ» _ β†’ acc)

\end{code}

Singleton sets can be constructed as follows.

\begin{code}

❴_❡ : (A : 𝕍) β†’ 𝕍
❴ A ❡ = 𝕍-ssup πŸ™ (Ξ» _ β†’ A) (global-point-is-embedding (Ξ» _ β†’ A) 𝕍-is-set)

❴❡-behaviour : (A : 𝕍) (B : 𝕍) β†’ B ∈ ❴ A ❡ ≃ (B ＝ A)
❴❡-behaviour A B = B ∈ ❴ A ❡    β‰ƒβŸ¨ ∈-behaviour' B ❴ A ❡ ⟩
                   πŸ™ Γ— (A ＝ B) β‰ƒβŸ¨ πŸ™-lneutral ⟩
                   (A ＝ B)     β‰ƒβŸ¨ ＝-flip ⟩
                   (B ＝ A)     β– 

\end{code}

Given a family of iterative sets indexed by a small type, we construct
its union as in [4].

We make use of propositional truncations (to define the image of a
map) and of set replacement (which follows from having set quotients).

\begin{code}

open import UF.PropTrunc

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

 open PropositionalTruncation pt
 open import UF.ImageAndSurjection pt

 module unions-of-iterative-sets (sr : Set-Replacement pt) where

  private
   module union-construction
          {I : 𝓀 Μ‡ }
          (𝓐 : I β†’ 𝕍)
         where

    im : 𝓀⁺ Μ‡
    im = image 𝓐

    im-is-small : image 𝓐 is 𝓀 small
    im-is-small = sr 𝓐 (I , ≃-refl I) 𝕍-is-locally-small 𝕍-is-set

    im⁻ : 𝓀 Μ‡
    im⁻ = resized im im-is-small

    im⁻-≃-im : im⁻ ≃ im
    im⁻-≃-im = resizing-condition im-is-small

    Ο€ : im β†’ 𝕍
    Ο€ = restriction 𝓐

    π⁻ : im⁻ β†’ 𝕍
    π⁻ = Ο€ ∘ ⌜ im⁻-≃-im ⌝

    Ο€-is-embedding : is-embedding Ο€
    Ο€-is-embedding = restrictions-are-embeddings 𝓐

    π⁻-is-embedding : is-embedding π⁻
    π⁻-is-embedding = ∘-is-embedding
                       (equivs-are-embeddings
                         ⌜ im⁻-≃-im ⌝
                         (⌜⌝-is-equiv im⁻-≃-im))
                       Ο€-is-embedding

  ⋃ : {I : 𝓀 Μ‡ } (𝓐 : I β†’ 𝕍) β†’ 𝕍
  ⋃ {I} 𝓐 = 𝕍-ssup im⁻ π⁻ π⁻-is-embedding
   where
    open union-construction 𝓐

  ⋃-behaviour : {I : 𝓀 Μ‡ } (𝓐 : I β†’ 𝕍) (B : 𝕍)
              β†’ B ∈ ⋃ 𝓐 ≃ (βˆƒ i κž‰ I , B ＝ 𝓐 i)
  ⋃-behaviour {I} 𝓐 B =
   B ∈ ⋃ 𝓐                                    β‰ƒβŸ¨ ∈-behaviour' B (⋃ 𝓐) ⟩
   (Ξ£ j κž‰ im⁻ , π⁻ j ＝ B)                    β‰ƒβŸ¨ e₁ ⟩
   (Ξ£ j κž‰ im , Ο€ j ＝ B)                      β‰ƒβŸ¨ Ξ£-assoc ⟩
   (Ξ£ C κž‰ 𝕍 , C ∈image 𝓐 Γ— (C ＝ B))          β‰ƒβŸ¨ Ξ£-cong (Ξ» C β†’ Γ—-comm) ⟩
   (Ξ£ C κž‰ 𝕍 , (C ＝ B) Γ— (C ∈image 𝓐))        β‰ƒβŸ¨ ≃-sym Ξ£-assoc ⟩
   (Ξ£ s κž‰ singleton-type' B , pr₁ s ∈image 𝓐) β‰ƒβŸ¨ ≃-sym eβ‚‚ ⟩
   πŸ™ {𝓀} Γ— B ∈image 𝓐                         β‰ƒβŸ¨ πŸ™-lneutral ⟩
   (βˆƒ i κž‰ I , 𝓐 i ＝ B)                       β‰ƒβŸ¨ βˆƒ-cong pt (Ξ» i β†’ ＝-flip) ⟩
   (βˆƒ i κž‰ I , B ＝ 𝓐 i)                       β– 
    where
     open union-construction 𝓐
     e₁ = Ξ£-change-of-variable-≃ _ im⁻-≃-im
     eβ‚‚ = Ξ£-change-of-variable-≃ _
           (singleton-≃-πŸ™' (singleton-types'-are-singletons B))

\end{code}

Any iterative set is the union of its 𝕍-forest.

\begin{code}

  ⋃-Ξ· : (A : 𝕍) β†’ ⋃ (𝕍-forest A) ＝ A
  ⋃-Ξ· A = ∈-is-extensional (⋃ (𝕍-forest A)) A i j
   where
    i : ⋃ (𝕍-forest A) βŠ† A
    i B m = βˆ₯βˆ₯-rec (∈-is-prop-valued B A) f (⌜ ⋃-behaviour (𝕍-forest A) B ⌝ m)
     where
      f : (Ξ£ a κž‰ 𝕍-root A , B ＝ 𝕍-forest A a) β†’ B ∈ A
      f (a , refl) = 𝕍-forest-∈ A a
    j : A βŠ† ⋃ (𝕍-forest A)
    j B m = ⌜ ⋃-behaviour (𝕍-forest A) B ⌝⁻¹ ∣ a , e ∣
     where
      abstract
       m' : Ξ£ a κž‰ 𝕍-root A , 𝕍-forest A a ＝ B
       m' = ⌜ ∈-behaviour' B A ⌝ m
       a : 𝕍-root A
       a = pr₁ m'
       e : B ＝ 𝕍-forest A a
       e = (prβ‚‚ m') ⁻¹

\end{code}

Unions allow us to construct a retraction of the inclusion 𝕍 β†ͺ 𝕄, and
this seems to be a new result.

\begin{code}

  𝕄-to-𝕍 : 𝕄 β†’ 𝕍
  𝕄-to-𝕍 (ssup X Ο†) = ⋃ (𝕄-to-𝕍 ∘ Ο†)

  𝕄-to-𝕍-is-retraction-of-inclusion : 𝕄-to-𝕍 ∘ underlying-mset ＝ id
  𝕄-to-𝕍-is-retraction-of-inclusion = dfunext fe (∈-induction _ f)
   where
    f : (A : 𝕍) β†’ ((B : 𝕍) β†’ B ∈ A β†’ (𝕄-to-𝕍 ∘ underlying-mset) B ＝ B)
      β†’ (𝕄-to-𝕍 ∘ underlying-mset) A ＝ A
    f A IH = 𝕄-to-𝕍 Aβ‚˜                                 ＝⟨ I ⟩
             𝕄-to-𝕍 (ssup (𝕍-root A) (𝕄-forest Aβ‚˜))    ＝⟨refl⟩
             ⋃ (𝕄-to-𝕍 ∘ 𝕄-forest Aβ‚˜)                  ＝⟨refl⟩
             ⋃ (𝕄-to-𝕍 ∘ underlying-mset ∘ 𝕍-forest A) ＝⟨ II ⟩
             ⋃ (𝕍-forest A)                            ＝⟨ ⋃-Ξ· A ⟩
             A                                         ∎
              where
               Aβ‚˜ : 𝕄
               Aβ‚˜ = underlying-mset A
               I  = ap (𝕄-to-𝕍 ∘ underlying-mset) (𝕍-Ξ· A ⁻¹)
               II = ap ⋃ (dfunext fe (Ξ» a β†’ IH (𝕍-forest A a) (𝕍-forest-∈ A a)))

  𝕍-is-retract-of-𝕄 : retract 𝕍 of 𝕄
  𝕍-is-retract-of-𝕄 = 𝕄-to-𝕍 ,
                      underlying-mset ,
                      happly 𝕄-to-𝕍-is-retraction-of-inclusion

\end{code}