Families of types over telescopes

Content created by Fredrik Bakke.

Created on 2024-03-19.
Last modified on 2024-03-19.

module foundation.families-over-telescopes where
open import elementary-number-theory.natural-numbers

open import foundation.raising-universe-levels
open import foundation.telescopes
open import foundation.universe-levels


A type family over a telescope is a family of types defined in the context of the telescope.

For instance, given a length three telescope

  Γ := ⟨x : A, y : B x, z : C x y z⟩

a type family over Γ is a ternary family of types

  D : (x : A) (y : B x) (z : C x y z) → 𝒰.


Type families over telescopes

family-over-telescope :
  {l1 : Level} (l2 : Level) {n : }  telescope l1 n  UU (l1  lsuc l2)
family-over-telescope {l1} l2 (base-telescope X) =
  raise (l1  lsuc l2) (UU l2)
family-over-telescope l2 (cons-telescope {X = X} Γ) =
  (x : X)  family-over-telescope l2 (Γ x)

Recent changes