Cumulative hierarchy

Content created by Fredrik Bakke, Fernando Chu, Jonathan Prieto-Cubides and Egbert Rijke.

Created on 2023-02-19.
Last modified on 2023-09-11.

module set-theory.cumulative-hierarchy where
Imports
open import elementary-number-theory.natural-numbers

open import foundation.action-on-identifications-functions
open import foundation.booleans
open import foundation.cartesian-product-types
open import foundation.constant-type-families
open import foundation.coproduct-types
open import foundation.dependent-pair-types
open import foundation.empty-types
open import foundation.existential-quantification
open import foundation.function-types
open import foundation.functoriality-propositional-truncation
open import foundation.identity-types
open import foundation.logical-equivalences
open import foundation.negation
open import foundation.propositional-extensionality
open import foundation.propositional-truncations
open import foundation.propositions
open import foundation.raising-universe-levels
open import foundation.sets
open import foundation.transport-along-identifications
open import foundation.truncated-types
open import foundation.unit-type
open import foundation.universe-levels

Idea

The cumulative hierarchy is a model of set theory. Instead of introducing it as a HIT, as in the HoTT Book Section 10.4, we introduce its induction principle, following Reference 2 below.

Definitions

Smaller image

has-smaller-image :
  { l1 l2 l3 : Level} 
  {A : UU l1} {B : UU l2} {C : UU l3} 
  (A  C)  (B  C)  UU (l1  l2  l3)
has-smaller-image {l1} {l2} {l3} {A} {B} {C} f g =
  (a : A)   B  b  g b  f a)

has-same-image :
  { l1 l2 l3 : Level} 
  {A : UU l1} {B : UU l2} {C : UU l3} 
  (A  C)  (B  C)  UU (l1  l2  l3)
has-same-image {l1} {l2} {l3} {A} {B} {C} f g =
  has-smaller-image f g ×
    has-smaller-image g f

Pseudo cumulative hierarchy

A type is a pseudo cumulative hierarchy if it has the structure of a cumulative hierarchy, but not necessarily its induction principle.

has-cumulative-hierarchy-structure :
  {l : Level}  (V : UU (lsuc l))  UU (lsuc l)
has-cumulative-hierarchy-structure {l} V =
  ( is-set V) ×
    ( Σ ({A : UU l}  (A  V)  V)
      ( λ V-set 
        ( {A B : UU l} (f : A  V) (g : B  V) 
          ( has-same-image f g)  V-set f  V-set g)))

pseudo-cumulative-hierarchy : (l : Level)  UU (lsuc (lsuc l))
pseudo-cumulative-hierarchy (l) =
  Σ (UU (lsuc l)) has-cumulative-hierarchy-structure

module _
  {l : Level} (V : pseudo-cumulative-hierarchy l)
  where

  type-pseudo-cumulative-hierarchy : UU (lsuc l)
  type-pseudo-cumulative-hierarchy = pr1 V

  is-set-pseudo-cumulative-hierarchy :
    is-set type-pseudo-cumulative-hierarchy
  is-set-pseudo-cumulative-hierarchy = pr1 (pr2 V)

  set-pseudo-cumulative-hierarchy :
    { A : UU l} 
    ( A  type-pseudo-cumulative-hierarchy) 
    type-pseudo-cumulative-hierarchy
  set-pseudo-cumulative-hierarchy = pr1 (pr2 (pr2 V))

  set-ext-pseudo-cumulative-hierarchy :
    { A B : UU l} (f : A  type-pseudo-cumulative-hierarchy)
    ( g : B  type-pseudo-cumulative-hierarchy) 
    ( has-same-image f g) 
    set-pseudo-cumulative-hierarchy f  set-pseudo-cumulative-hierarchy g
  set-ext-pseudo-cumulative-hierarchy = pr2 (pr2 (pr2 V))

The induction principle and computation rule of the cumulative hierarchy

module _
  {l1 : Level} (l2 : Level) (V : pseudo-cumulative-hierarchy l1)
  where
  induction-principle-cumulative-hierarchy : UU (lsuc (l1  l2))
  induction-principle-cumulative-hierarchy =
    ( P : type-pseudo-cumulative-hierarchy V  UU l2) 
    ( (x : type-pseudo-cumulative-hierarchy V)  is-set (P x)) 
    ( ρ :
      { A : UU l1} (f : A  type-pseudo-cumulative-hierarchy V) 
      ( (a : A)  P (f a))  P (set-pseudo-cumulative-hierarchy V f)) 
    ( { A B : UU l1} (f : A  type-pseudo-cumulative-hierarchy V) 
      ( g : B  type-pseudo-cumulative-hierarchy V)
      ( e : has-same-image f g)
      ( IH₁ : (a : A)  P (f a))
      ( IH₂ : (b : B)  P (g b)) 
      ( ( a : A)   B  b  Σ (f a  g b)
        ( λ p  tr P p (IH₁ a)  IH₂ b))) 
      ( ( b : B)   A  a 
        Σ (g b  f a)  p  tr P p (IH₂ b)  IH₁ a))) 
      tr P (set-ext-pseudo-cumulative-hierarchy V f g e) (ρ f IH₁)  ρ g IH₂) 
    (x : type-pseudo-cumulative-hierarchy V)  P x

  compute-induction-principle-cumulative-hierarchy :
    induction-principle-cumulative-hierarchy  UU (lsuc (l1  l2))
  compute-induction-principle-cumulative-hierarchy IP =
    ( P : type-pseudo-cumulative-hierarchy V  UU l2) 
    ( σ : (x : type-pseudo-cumulative-hierarchy V)  is-set (P x)) 
    ( ρ :
      { A : UU l1} (f : A  type-pseudo-cumulative-hierarchy V) 
      ( (a : A)  P (f a))  P (set-pseudo-cumulative-hierarchy V f)) 
    ( τ :
      { A B : UU l1} (f : A  type-pseudo-cumulative-hierarchy V) 
      ( g : B  type-pseudo-cumulative-hierarchy V)
      ( e : has-same-image f g)
      ( IH₁ : (a : A)  P (f a))
      ( IH₂ : (b : B)  P (g b)) 
      ( (a : A)   B  b  Σ (f a  g b)
        ( λ p  tr P p (IH₁ a)  IH₂ b))) 
      ( (b : B)   A  a  Σ (g b  f a)
         p  tr P p (IH₂ b)  IH₁ a))) 
      tr P (set-ext-pseudo-cumulative-hierarchy V f g e) (ρ f IH₁)  ρ g IH₂) 
    { A : UU l1} (f : A  type-pseudo-cumulative-hierarchy V)
    ( IH : (a : A)  P (f a)) 
    IP P σ ρ τ (set-pseudo-cumulative-hierarchy V f)  ρ f IH

Examples

module _
  {l1 : Level} (V : pseudo-cumulative-hierarchy l1)
  (induction-principle-cumulative-hierarchy-V :
    (l2 : Level)  induction-principle-cumulative-hierarchy l2 V)
  (compute-induction-principle-cumulative-hierarchy-V :
    (l2 : Level)  compute-induction-principle-cumulative-hierarchy l2 V
      (induction-principle-cumulative-hierarchy-V l2))
  where

The empty set

  empty-set-cumulative-hierarchy : type-pseudo-cumulative-hierarchy V
  empty-set-cumulative-hierarchy =
    set-pseudo-cumulative-hierarchy V (raise-ex-falso l1)

The set containing only the empty set

  set-empty-set-cumulative-hierarchy : type-pseudo-cumulative-hierarchy V
  set-empty-set-cumulative-hierarchy =
    set-pseudo-cumulative-hierarchy V {raise-unit l1}
      ( λ _  empty-set-cumulative-hierarchy)

Properties

Every element of the cumulative hierarchy is given by a function into the cumulative hierarchy

  underlying-function-cumulative-hierarchy :
    (v : type-pseudo-cumulative-hierarchy V) 
     ( UU l1)
      ( λ A 
        Σ ( A  type-pseudo-cumulative-hierarchy V)
          ( λ f  set-pseudo-cumulative-hierarchy V f  v))
  underlying-function-cumulative-hierarchy =
    induction-principle-cumulative-hierarchy-V
      ( lsuc l1) _
      ( λ _  is-trunc-type-Truncated-Type (set-trunc-Prop _))
      ( λ {A} f H  unit-trunc-Prop (pair A (pair f refl)))
      ( λ f g e IH₁ IH₂ hIH₁ hIH₂  eq-is-prop is-prop-type-trunc-Prop)

The induction principle simplified for families of propositions

  prop-ind-principle-cumulative-hierarchy :
    { l2 : Level}
    ( P : type-pseudo-cumulative-hierarchy V  UU l2) 
    ( ( x : type-pseudo-cumulative-hierarchy V)  is-prop (P x)) 
    ( { A : UU l1} (f : A  type-pseudo-cumulative-hierarchy V) 
      ( (a : A)  P (f a)) 
      ( P (set-pseudo-cumulative-hierarchy V f))) 
    ( x : type-pseudo-cumulative-hierarchy V)  P x
  prop-ind-principle-cumulative-hierarchy {l2} P σ ρ =
    induction-principle-cumulative-hierarchy-V l2 P
      ( λ x  is-set-is-prop (σ x)) ρ
      ( λ _ g _ _ _ _ _  eq-is-prop (σ (set-pseudo-cumulative-hierarchy V g)))

  compute-prop-ind-principle-cumulative-hierarchy :
    { l2 : Level}
    ( P : type-pseudo-cumulative-hierarchy V  UU l2) 
    ( σ : ( x : type-pseudo-cumulative-hierarchy V)  is-prop (P x)) 
    ( ρ :
      { A : UU l1} (f : A  type-pseudo-cumulative-hierarchy V) 
      ( (a : A)  P (f a)) 
      ( P (set-pseudo-cumulative-hierarchy V f))) 
    { A : UU l1} (f : A  type-pseudo-cumulative-hierarchy V)
    ( IH : (a : A)  P (f a)) 
    prop-ind-principle-cumulative-hierarchy
      P σ ρ (set-pseudo-cumulative-hierarchy V f)  ρ f IH
  compute-prop-ind-principle-cumulative-hierarchy {l2} P σ ρ =
    compute-induction-principle-cumulative-hierarchy-V l2 P
      ( λ x  is-set-is-prop (σ x)) ρ
      ( λ _ g _ _ _ _ _  eq-is-prop (σ (set-pseudo-cumulative-hierarchy V g)))

The recursion principle and its computation rule for the cumulative hierarchy

  recursion-principle-cumulative-hierarchy :
    { l2 : Level}
    ( X : UU l2) (σ : is-set X)
    ( ρ : {A : UU l1}  (A  type-pseudo-cumulative-hierarchy V)  (A  X)  X)
    ( τ :
      { A B : UU l1} (f : A  type-pseudo-cumulative-hierarchy V)
      ( g : B  type-pseudo-cumulative-hierarchy V)
      ( e : has-same-image f g)
      ( IH₁ : A  X)
      ( IH₂ : B  X) 
      ( (a : A)   B  b  (f a  g b) × (IH₁ a  IH₂ b))) 
      ( (b : B)   A  a  (g b  f a) × (IH₂ b  IH₁ a))) 
      ρ f IH₁  ρ g IH₂) 
    type-pseudo-cumulative-hierarchy V  X
  recursion-principle-cumulative-hierarchy {l2} X σ ρ τ =
    induction-principle-cumulative-hierarchy-V l2  _  X)  _  σ) ρ τ'
    where
    τ' :
      { A B : UU l1} (f : A  pr1 V) (g : B  pr1 V)
      ( e : has-same-image f g)
      ( IH₁ : (a : A)  X) (IH₂ : (b : B)  X) 
      ( (a : A)   B  b  Σ (f a  g b)
         p  tr  _  X) p (IH₁ a)  IH₂ b))) 
      ( (b : B)   A  a  Σ (g b  f a)
         p  tr  _  X) p (IH₂ b)  IH₁ a))) 
      tr  _  X) (pr2 (pr2 (pr2 V)) f g e) (ρ f IH₁)  ρ g IH₂
    τ' {A} {B} f g e IH₁ IH₂ hIH₁ hIH₂ =
      equational-reasoning
        tr  _  X) (pr2 (pr2 (pr2 V)) f g e) (ρ f IH₁)
         ρ f IH₁
          by tr-constant-type-family path-f-g (ρ f IH₁)
         ρ g IH₂
          by τ f g e IH₁ IH₂ hIH₁' hIH₂'
      where
      path-f-g :
        set-pseudo-cumulative-hierarchy V f
           set-pseudo-cumulative-hierarchy V g
      path-f-g = set-ext-pseudo-cumulative-hierarchy V f g e
      hIH₁' : (a : A)   B  b  Σ (f a  g b)  _  IH₁ a  IH₂ b))
      hIH₁' a =
        map-trunc-Prop
          ( λ (b , p , q) 
            ( b , p , (inv (tr-constant-type-family p _)  q)))
          ( hIH₁ a)
      hIH₂' : (b : B)   A  a  Σ (g b  f a)  _  IH₂ b  IH₁ a))
      hIH₂' b =
        map-trunc-Prop
          ( λ (a , p , q) 
            ( a , p , (inv (tr-constant-type-family p _)  q)))
          ( hIH₂ b)

  compute-recursion-principle-cumulative-hierarchy :
    { l2 : Level} ( X : UU l2) (σ : is-set X)
    ( ρ : {A : UU l1}  (A  type-pseudo-cumulative-hierarchy V)  (A  X)  X)
    ( τ :
      { A B : UU l1} (f : A  type-pseudo-cumulative-hierarchy V)
      ( g : B  type-pseudo-cumulative-hierarchy V)
      ( e : has-same-image f g)
      ( IH₁ : A  X)
      ( IH₂ : B  X) 
      ( ( a : A)   B  b  (f a  g b) × (IH₁ a  IH₂ b))) 
      ( ( b : B)   A  a  (g b  f a) × (IH₂ b  IH₁ a))) 
      ρ f IH₁  ρ g IH₂) 
    {A : UU l1}  (f : A  type-pseudo-cumulative-hierarchy V)  (IH : A  X) 
    recursion-principle-cumulative-hierarchy X σ ρ τ
      ( set-pseudo-cumulative-hierarchy V f)  ρ f IH
  compute-recursion-principle-cumulative-hierarchy {l2} X σ ρ τ =
    compute-induction-principle-cumulative-hierarchy-V
      l2  _  X)  _  σ) ρ τ'
    where
    τ' :
      { A B : UU l1} (f : A  pr1 V) (g : B  pr1 V)
      ( e : has-same-image f g)
      ( IH₁ : (a : A)  X) (IH₂ : (b : B)  X) 
      ( ( a : A)   B  b  Σ (f a  g b)
        ( λ p  tr  _  X) p (IH₁ a)  IH₂ b))) 
      ( ( b : B)   A  a  Σ (g b  f a)
        ( λ p  tr  _  X) p (IH₂ b)  IH₁ a))) 
      tr  _  X) (pr2 (pr2 (pr2 V)) f g e) (ρ f IH₁)  ρ g IH₂
    τ' {A} {B} f g e IH₁ IH₂ hIH₁ hIH₂ =
      equational-reasoning
        tr  _  X) (pr2 (pr2 (pr2 V)) f g e) (ρ f IH₁)
         ρ f IH₁
          by tr-constant-type-family path-f-g (ρ f IH₁)
         ρ g IH₂
          by τ f g e IH₁ IH₂ hIH₁' hIH₂'
      where
      path-f-g :
        set-pseudo-cumulative-hierarchy V f
           set-pseudo-cumulative-hierarchy V g
      path-f-g = set-ext-pseudo-cumulative-hierarchy V f g e
      hIH₁' : (a : A)   B  b  Σ (f a  g b)  _  IH₁ a  IH₂ b))
      hIH₁' a =
        map-trunc-Prop
          ( λ (b , p , q) 
            ( b , p , (inv (tr-constant-type-family p _)  q)))
          ( hIH₁ a)
      hIH₂' : (b : B)   A  a  Σ (g b  f a)  _  IH₂ b  IH₁ a))
      hIH₂' b =
        map-trunc-Prop
          ( λ (a , p , q) 
            ( a , p , (inv (tr-constant-type-family p _)  q)))
          ( hIH₂ b)

A simplification of the recursion principle, when the codomain is Prop l2.

  prop-recursion-principle-cumulative-hierarchy :
    {l2 : Level}
    ( ρ :
      { A : UU l1}  (A  type-pseudo-cumulative-hierarchy V) 
      ( A  Prop l2)  Prop l2)
    ( τ : {A B : UU l1} (f : A  type-pseudo-cumulative-hierarchy V)
      ( g : B  type-pseudo-cumulative-hierarchy V)
      ( e : has-smaller-image f g)
      ( IH₁ : A  Prop l2)
      ( IH₂ : B  Prop l2) 
      ( (a : A)   B  b  (f a  g b) × (IH₁ a  IH₂ b))) 
      type-Prop (ρ f IH₁)  type-Prop (ρ g IH₂)) 
    type-pseudo-cumulative-hierarchy V  Prop l2
  prop-recursion-principle-cumulative-hierarchy {l2} ρ τ =
    recursion-principle-cumulative-hierarchy (Prop l2)
      is-set-type-Prop ρ τ'
    where
    τ' :
      { A B : UU l1} (f : A  type-pseudo-cumulative-hierarchy V)
      ( g : B  type-pseudo-cumulative-hierarchy V) 
      ( e : has-same-image f g)
      ( IH₁ : A  Prop l2) (IH₂ : B  Prop l2) 
      ( (a : A)   B  b  (f a  g b) × (IH₁ a  IH₂ b))) 
      ( (b : B)   A  a  (g b  f a) × (IH₂ b  IH₁ a))) 
      ρ f IH₁  ρ g IH₂
    τ' f g (e₁ , e₂) IH₁ IH₂ hIH₁ hIH₂ =
      eq-iff (τ f g e₁ IH₁ IH₂ hIH₁) (τ g f e₂ IH₂ IH₁ hIH₂)

  compute-prop-recursion-principle-cumulative-hierarchy :
    {l2 : Level}
    ( ρ :
      { A : UU l1}  (A  type-pseudo-cumulative-hierarchy V) 
      ( A  Prop l2)  Prop l2)
    ( τ :
      { A B : UU l1} (f : A  type-pseudo-cumulative-hierarchy V)
      ( g : B  type-pseudo-cumulative-hierarchy V)
      ( e : has-smaller-image f g)
      ( IH₁ : A  Prop l2)
      ( IH₂ : B  Prop l2) 
      ( (a : A)   B  b  (f a  g b) × (IH₁ a  IH₂ b))) 
      type-Prop (ρ f IH₁)  type-Prop (ρ g IH₂)) 
    { A : UU l1}  (f : A  type-pseudo-cumulative-hierarchy V) 
    ( IH : A  Prop l2) 
    prop-recursion-principle-cumulative-hierarchy ρ τ
      ( set-pseudo-cumulative-hierarchy V f)  ρ f IH
  compute-prop-recursion-principle-cumulative-hierarchy {l2} ρ τ =
    compute-recursion-principle-cumulative-hierarchy (Prop l2)
      is-set-type-Prop ρ τ'
    where
    τ' :
      { A B : UU l1} (f : A  type-pseudo-cumulative-hierarchy V)
      ( g : B  type-pseudo-cumulative-hierarchy V) 
      ( e : has-same-image f g)
      ( IH₁ : A  Prop l2) (IH₂ : B  Prop l2) 
      ( (a : A)   B  b  (f a  g b) × (IH₁ a  IH₂ b))) 
      ( (b : B)   A  a  (g b  f a) × (IH₂ b  IH₁ a))) 
      ρ f IH₁  ρ g IH₂
    τ' f g (e₁ , e₂) IH₁ IH₂ hIH₁ hIH₂ =
      eq-iff (τ f g e₁ IH₁ IH₂ hIH₁) (τ g f e₂ IH₂ IH₁ hIH₂)

Another simplification of the recursion principle, when recursive calls are not needed.

  simple-prop-recursion-principle-cumulative-hierarchy :
    {l2 : Level}
    ( ρ : {A : UU l1}  (A  type-pseudo-cumulative-hierarchy V)  Prop l2)
    ( τ :
      { A B : UU l1} (f : A  type-pseudo-cumulative-hierarchy V)
      ( g : B  type-pseudo-cumulative-hierarchy V) 
      ( e : has-smaller-image f g) 
      type-Prop (ρ f)  type-Prop (ρ g)) 
    type-pseudo-cumulative-hierarchy V  Prop l2
  simple-prop-recursion-principle-cumulative-hierarchy {l2} ρ τ =
    prop-recursion-principle-cumulative-hierarchy
      ( λ f _  ρ f)  f g e _ _ _  τ f g e)

  compute-simple-prop-recursion-principle-cumulative-hierarchy :
    {l2 : Level}
    ( ρ : {A : UU l1}  (A  type-pseudo-cumulative-hierarchy V)  Prop l2)
    ( τ :
      { A B : UU l1} (f : A  type-pseudo-cumulative-hierarchy V)
      ( g : B  type-pseudo-cumulative-hierarchy V) 
      ( e : has-smaller-image f g) 
      type-Prop (ρ f)  type-Prop (ρ g)) 
    {A : UU l1}  (f : A  type-pseudo-cumulative-hierarchy V) 
    simple-prop-recursion-principle-cumulative-hierarchy ρ τ
      ( set-pseudo-cumulative-hierarchy V f)  ρ f
  compute-simple-prop-recursion-principle-cumulative-hierarchy {l2} ρ τ f =
    compute-prop-recursion-principle-cumulative-hierarchy
      ( λ f _  ρ f)  f g e _ _ _  τ f g e) f  _  raise-Prop l2 unit-Prop)

The membership relationship for the cumulative hierarchy

  ∈-cumulative-hierarchy-Prop :
    ( type-pseudo-cumulative-hierarchy V) 
    ( type-pseudo-cumulative-hierarchy V) 
    Prop (lsuc l1)
  ∈-cumulative-hierarchy-Prop x =
    simple-prop-recursion-principle-cumulative-hierarchy
       {A} f  ( A  a  f a  x)) , is-prop-∃ _ _) e
    where
    e :
      {A B : UU l1} (f : A  type-pseudo-cumulative-hierarchy V)
      ( g : B  type-pseudo-cumulative-hierarchy V) 
      ( e : has-smaller-image f g) 
      (  A  a  f a  x)   B  b  g b  x))
    e {A} {B} f g s =
      map-universal-property-trunc-Prop
        ( ∃-Prop B  b  g b  x))
        ( λ ( a , p) 
          map-trunc-Prop  (b , q)  (b , q  p)) (s a))

  ∈-cumulative-hierarchy :
    ( type-pseudo-cumulative-hierarchy V) 
    ( type-pseudo-cumulative-hierarchy V) 
    UU (lsuc l1)
  ∈-cumulative-hierarchy x y =
    type-Prop (∈-cumulative-hierarchy-Prop x y)

  id-∈-cumulative-hierarchy :
    ( x : type-pseudo-cumulative-hierarchy V) {A : UU l1}
    ( f : A  type-pseudo-cumulative-hierarchy V) 
    ( ∈-cumulative-hierarchy x (set-pseudo-cumulative-hierarchy V f)) 
       A  a  f a  x)
  id-∈-cumulative-hierarchy x f =
    ap pr1 (compute-simple-prop-recursion-principle-cumulative-hierarchy _ _ f)

  ∈-cumulative-hierarchy-mere-preimage :
    { x : type-pseudo-cumulative-hierarchy V} 
    { A : UU l1}
    { f : A  type-pseudo-cumulative-hierarchy V} 
    ( ∈-cumulative-hierarchy x (set-pseudo-cumulative-hierarchy V f)) 
     A  a  f a  x)
  ∈-cumulative-hierarchy-mere-preimage {x} {A} {f} =
    tr id (id-∈-cumulative-hierarchy x f)

  mere-preimage-∈-cumulative-hierarchy :
    { x : type-pseudo-cumulative-hierarchy V} 
    { A : UU l1}
    { f : A  type-pseudo-cumulative-hierarchy V} 
     A  a  f a  x) 
    ( ∈-cumulative-hierarchy x (set-pseudo-cumulative-hierarchy V f))
  mere-preimage-∈-cumulative-hierarchy {x} {A} {f} =
    tr id (inv (id-∈-cumulative-hierarchy x f))

  is-prop-∈-cumulative-hierarchy :
    ( x : type-pseudo-cumulative-hierarchy V) 
    ( y : type-pseudo-cumulative-hierarchy V) 
    is-prop (∈-cumulative-hierarchy x y)
  is-prop-∈-cumulative-hierarchy x y =
    is-prop-type-Prop (∈-cumulative-hierarchy-Prop x y)

The subset relationship for the cumulative hierarchy

  ⊆-cumulative-hierarchy :
    ( type-pseudo-cumulative-hierarchy V) 
    ( type-pseudo-cumulative-hierarchy V) 
    UU (lsuc l1)
  ⊆-cumulative-hierarchy x y =
    ( v : type-pseudo-cumulative-hierarchy V) 
    ∈-cumulative-hierarchy v x  ∈-cumulative-hierarchy v y

  is-prop-⊆-cumulative-hierarchy :
    ( x : type-pseudo-cumulative-hierarchy V) 
    ( y : type-pseudo-cumulative-hierarchy V) 
    is-prop (⊆-cumulative-hierarchy x y)
  is-prop-⊆-cumulative-hierarchy x y =
    is-prop-Π ( λ v 
      ( is-prop-Π  _  is-prop-∈-cumulative-hierarchy v y)))

  ⊆-cumulative-hierarchy-has-smaller-image :
    { A B : UU l1}
    ( f : A  type-pseudo-cumulative-hierarchy V)
    ( g : B  type-pseudo-cumulative-hierarchy V) 
    ⊆-cumulative-hierarchy
      ( set-pseudo-cumulative-hierarchy V f)
      ( set-pseudo-cumulative-hierarchy V g) 
    has-smaller-image f g
  ⊆-cumulative-hierarchy-has-smaller-image f g s a =
    ∈-cumulative-hierarchy-mere-preimage
      ( s (f a)
        ( mere-preimage-∈-cumulative-hierarchy
          (unit-trunc-Prop (a , refl))))

  has-smaller-image-⊆-cumulative-hierarchy :
    { A B : UU l1}
    ( f : A  type-pseudo-cumulative-hierarchy V)
    ( g : B  type-pseudo-cumulative-hierarchy V) 
    has-smaller-image f g 
    ⊆-cumulative-hierarchy
      ( set-pseudo-cumulative-hierarchy V f)
      ( set-pseudo-cumulative-hierarchy V g)
  has-smaller-image-⊆-cumulative-hierarchy {A} {B} f g s x m =
    mere-preimage-∈-cumulative-hierarchy
      ( map-universal-property-trunc-Prop (∃-Prop B  b  g b  x))
        ( λ (a , p) 
          map-trunc-Prop  (b , q)  (b , q  p)) (s a))
        ( ∈-cumulative-hierarchy-mere-preimage m))

Extensionality of the membership relation

  pre-extensionality-∈-cumulative-hierarchy :
    { A : UU l1}
    ( f : A  type-pseudo-cumulative-hierarchy V)
    ( x : type-pseudo-cumulative-hierarchy V) 
    ( ⊆-cumulative-hierarchy x (set-pseudo-cumulative-hierarchy V f)) 
    ( ⊆-cumulative-hierarchy (set-pseudo-cumulative-hierarchy V f) x) 
    x  (set-pseudo-cumulative-hierarchy V f)
  pre-extensionality-∈-cumulative-hierarchy f =
    prop-ind-principle-cumulative-hierarchy
      ( λ x 
        ⊆-cumulative-hierarchy x (set-pseudo-cumulative-hierarchy V f) 
        ⊆-cumulative-hierarchy (set-pseudo-cumulative-hierarchy V f) x 
        x  (set-pseudo-cumulative-hierarchy V f))
      ( λ v 
        is-prop-Π  _ 
          is-prop-Π  _ 
            is-set-pseudo-cumulative-hierarchy V
              v (set-pseudo-cumulative-hierarchy V f))))
      ( λ g H H₁ H₂ 
        set-ext-pseudo-cumulative-hierarchy V g f
          ( ⊆-cumulative-hierarchy-has-smaller-image g f H₁ ,
            ⊆-cumulative-hierarchy-has-smaller-image f g H₂))

  extensionality-∈-cumulative-hierarchy :
    ( x y : type-pseudo-cumulative-hierarchy V) 
    ( ⊆-cumulative-hierarchy x y) 
    ( ⊆-cumulative-hierarchy y x) 
    x  y
  extensionality-∈-cumulative-hierarchy x =
    prop-ind-principle-cumulative-hierarchy
      ( λ y 
        ⊆-cumulative-hierarchy x y 
        ⊆-cumulative-hierarchy y x  x  y)
      ( λ v 
        is-prop-Π  _ 
          is-prop-Π  _ 
            is-set-pseudo-cumulative-hierarchy V x v)))
      ( λ f H H₁ H₂ 
        pre-extensionality-∈-cumulative-hierarchy
          f x H₁ H₂)

Cumulative hierarchies satisfy the empty set axiom

  empty-set-axiom-cumulative-hierarchy :
    ( x : type-pseudo-cumulative-hierarchy V) 
    ¬ (∈-cumulative-hierarchy x empty-set-cumulative-hierarchy)
  empty-set-axiom-cumulative-hierarchy x H =
    map-universal-property-trunc-Prop empty-Prop
      ( λ (z , p)  raise-ex-falso l1 z)
      ( ∈-cumulative-hierarchy-mere-preimage H)

Cumulative hierarchies satisfy the pair axiom

  pair-cumulative-hierarchy :
    ( x y : type-pseudo-cumulative-hierarchy V) 
    type-pseudo-cumulative-hierarchy V
  pair-cumulative-hierarchy x y =
    set-pseudo-cumulative-hierarchy V bool-map
    where
    bool-map : raise-bool l1  type-pseudo-cumulative-hierarchy V
    bool-map (map-raise true) = x
    bool-map (map-raise false) = y

  pair-axiom-cumulative-hierarchy :
    ( x y v : type-pseudo-cumulative-hierarchy V) 
    ( ∈-cumulative-hierarchy v (pair-cumulative-hierarchy x y) 
      type-trunc-Prop ( (v  x) + (v  y)))
  pair-axiom-cumulative-hierarchy x y v =
    pair
      ( λ H  map-universal-property-trunc-Prop
        ( trunc-Prop ((v  x) + (v  y)))
        ( λ { ( map-raise true , p)  unit-trunc-Prop (inl (inv p)) ;
              ( map-raise false , p)  unit-trunc-Prop (inr (inv p))})
        ( ∈-cumulative-hierarchy-mere-preimage H))
      ( λ H  mere-preimage-∈-cumulative-hierarchy
        ( map-trunc-Prop
          ( λ { ( inl p)  (map-raise true , inv p) ;
                ( inr p)  (map-raise false , inv p)})
          ( H)))

Singleton function

  singleton-cumulative-hierarchy :
    type-pseudo-cumulative-hierarchy V 
    type-pseudo-cumulative-hierarchy V
  singleton-cumulative-hierarchy x =
    ( set-pseudo-cumulative-hierarchy V {raise-unit l1}
      ( λ _  x))

Cumulative hierarchies satisfy the infinity axiom

  infinity-cumulative-hierarchy : type-pseudo-cumulative-hierarchy V
  infinity-cumulative-hierarchy =
    set-pseudo-cumulative-hierarchy V ℕ-map
    where
    ℕ-map : raise l1   type-pseudo-cumulative-hierarchy V
    ℕ-map (map-raise zero-ℕ) = empty-set-cumulative-hierarchy
    ℕ-map (map-raise (succ-ℕ x)) =
      pair-cumulative-hierarchy
        ( ℕ-map (map-raise x))
        ( singleton-cumulative-hierarchy (ℕ-map (map-raise x)))

  infinity-axiom-cumulative-hierarchy :
    ( ∈-cumulative-hierarchy
        empty-set-cumulative-hierarchy
        infinity-cumulative-hierarchy) ×
    ( ( x : type-pseudo-cumulative-hierarchy V) 
      ∈-cumulative-hierarchy x infinity-cumulative-hierarchy 
      ∈-cumulative-hierarchy
        ( pair-cumulative-hierarchy x
          ( singleton-cumulative-hierarchy x))
        ( infinity-cumulative-hierarchy))
  infinity-axiom-cumulative-hierarchy =
    pair
      ( mere-preimage-∈-cumulative-hierarchy
        ( unit-trunc-Prop (map-raise zero-ℕ , refl)))
        ( λ x H 
          mere-preimage-∈-cumulative-hierarchy
            ( map-trunc-Prop
              ( λ {((map-raise n) , refl) 
                map-raise (succ-ℕ n) , refl})
            ( ∈-cumulative-hierarchy-mere-preimage H)))

Cumulative hierarchies satisfy the ∈-induction axiom

  ∈-induction-cumulative-hierarchy :
    {l2 : Level}
    ( P : type-pseudo-cumulative-hierarchy V  UU l2) 
    ( ( x : type-pseudo-cumulative-hierarchy V)  is-prop (P x)) 
    ( ( x : type-pseudo-cumulative-hierarchy V) 
      ( ( y : type-pseudo-cumulative-hierarchy V) 
        ∈-cumulative-hierarchy y x  P y) 
      P x) 
    ( x : type-pseudo-cumulative-hierarchy V)  P x
  ∈-induction-cumulative-hierarchy P P-prop h =
    prop-ind-principle-cumulative-hierarchy P P-prop
      ( λ f IH 
        h (set-pseudo-cumulative-hierarchy V f)
          ( λ y m 
            map-universal-property-trunc-Prop
              ( P y , P-prop y)
              ( λ (a , p)  tr P p (IH a))
              ( ∈-cumulative-hierarchy-mere-preimage m)))

Cumulative hierarchies satisfy the replacement axiom

  replacement-cumulative-hierarchy :
    ( x : type-pseudo-cumulative-hierarchy V) 
    ( r : type-pseudo-cumulative-hierarchy V 
      type-pseudo-cumulative-hierarchy V) 
     ( type-pseudo-cumulative-hierarchy V)
      ( λ v 
        ( y : type-pseudo-cumulative-hierarchy V) 
        ∈-cumulative-hierarchy y v 
         ( type-pseudo-cumulative-hierarchy V)
          ( λ z  (∈-cumulative-hierarchy z x) × (y  r z)))
  replacement-cumulative-hierarchy x r =
    map-universal-property-trunc-Prop
      ( ∃-Prop (type-pseudo-cumulative-hierarchy V) _)
      ( λ {(A , f , refl) 
        unit-trunc-Prop
          ( pair
            ( set-pseudo-cumulative-hierarchy V (r  f))
            ( λ y 
              ( pair
                ( λ H 
                  map-trunc-Prop
                    ( λ {(a , refl) 
                      pair (f a)
                        ( pair
                          ( mere-preimage-∈-cumulative-hierarchy
                            ( unit-trunc-Prop (a , refl)))
                          ( refl))})
                    ( ∈-cumulative-hierarchy-mere-preimage H))
                ( λ H  mere-preimage-∈-cumulative-hierarchy
                  ( map-universal-property-trunc-Prop
                    ( ∃-Prop A _)
                    ( λ {(z , K , refl) 
                      ( map-trunc-Prop
                        ( λ {(a , refl)  (a , refl)})
                        ( ∈-cumulative-hierarchy-mere-preimage K))})
                    ( H))))))})
      ( underlying-function-cumulative-hierarchy x)

References

  1. Univalent Foundations Project, Homotopy Type Theory – Univalent Foundations of Mathematics (2013) (website, arXiv:1308.0729, DOI:10.48550)
  2. Tom de Jong, in collaboration with Nicolai Kraus, Fredrik Nordvall Forsberg and Chuangjie Xu. https://www.cs.bham.ac.uk/~mhe/agda/UF.CumulativeHierarchy.html

Recent changes