Parametric types

Content created by Fredrik Bakke.

Created on 2026-03-06.
Last modified on 2026-03-06.

module foundation.parametric-types where
Imports 
open import foundation.dependent-pair-types
open import foundation.embeddings
open import foundation.empty-types
open import foundation.evaluation-functions
open import foundation.fibers-of-maps
open import foundation.propositional-maps
open import foundation.retracts-of-types
open import foundation.unit-type
open import foundation.universe-levels

open import foundation-core.contractible-types
open import foundation-core.equivalences
open import foundation-core.function-types
open import foundation-core.propositions

open import orthogonal-factorization-systems.null-types

Idea

A type X : 𝒰 is parametric if the constant map X → (𝒰 → X) is an equivalence. In other words, if X is 𝒰-null.

Definitions

The predicate on a type of being parametric

module _
  {l1 : Level} (l2 : Level) (X : UU l1)
  where

  is-parametric : UU (l1 ⊔ lsuc l2)
  is-parametric = is-null (UU l2) X

  is-prop-is-parametric : is-prop is-parametric
  is-prop-is-parametric = is-prop-is-null (UU l2) X

  is-parametric-Prop : Prop (l1 ⊔ lsuc l2)
  is-parametric-Prop = is-null-Prop (UU l2) X

The universe of parametric types

Parametric-Type : (l1 l2 : Level) → UU (lsuc l1 ⊔ lsuc l2)
Parametric-Type l1 l2 = Σ (UU l1) (is-parametric l2)

module _
  {l1 l2 : Level} (X : Parametric-Type l1 l2)
  where

  type-Parametric-Type : UU l1
  type-Parametric-Type = pr1 X

  is-parametric-type-Parametric-Type :
    is-parametric l2 type-Parametric-Type
  is-parametric-type-Parametric-Type = pr2 X

Properties

Contractible types are parametric

abstract
  is-parametric-is-contr :
    {l1 l2 : Level} {X : UU l1} →
    is-contr X → is-parametric l2 X
  is-parametric-is-contr {l2 = l2} =
    is-null-is-contr (UU l2)

The unit type is parametric

abstract
  is-parametric-unit :
    {l : Level} → is-parametric l unit
  is-parametric-unit {l} =
    is-parametric-is-contr is-contr-unit

The empty type is parametric

abstract
  is-parametric-empty :
    {l : Level} → is-parametric l empty
  is-parametric-empty {l} =
    is-equiv-is-empty _ (ev (raise-empty l))

Propositions are parametric

abstract
  is-parametric-is-prop :
    {l1 l2 : Level} {X : UU l1} →
    is-prop X → is-parametric l2 X
  is-parametric-is-prop {l1} {l2} H =
    is-null-is-prop H (ev (raise-empty l2))

Parametric types are closed under equivalences

module _
  {l1 l2 l3 : Level} {X : UU l1} {Y : UU l2}
  where abstract

  is-parametric-equiv :
    X ≃ Y → is-parametric l3 Y → is-parametric l3 X
  is-parametric-equiv = is-null-equiv-base

  is-parametric-equiv' :
    X ≃ Y → is-parametric l3 X → is-parametric l3 Y
  is-parametric-equiv' = is-null-equiv-base ∘ inv-equiv

Parametric types are closed under retracts

module _
  {l1 l2 l3 : Level} {X : UU l1} {Y : UU l2}
  where abstract

  is-parametric-retract :
    X retract-of Y → is-parametric l3 Y → is-parametric l3 X
  is-parametric-retract = is-null-retract-base

Parametric types are closed under embeddings

module _
  {l1 l2 l3 : Level} {X : UU l1} {Y : UU l2}
  where abstract

  is-parametric-emb :
    Y ↪ X → is-parametric l3 X → is-parametric l3 Y
  is-parametric-emb e is-parametric-X =
    is-parametric-equiv'
      ( equiv-total-fiber (map-emb e))
      ( is-null-Σ
        ( is-parametric-X)
        ( λ x → is-parametric-is-prop (is-prop-type-Prop (fiber-emb-Prop e x))))

See also

Recent changes