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
Imports 
open import elementary-number-theory.natural-numbers

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

Idea

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) → 𝒰.

Definitions

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