Multivariable correspondences

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

Created on 2022-09-09.
Last modified on 2025-01-06.

module foundation.multivariable-correspondences where
Imports 
open import elementary-number-theory.natural-numbers

open import foundation.universe-levels

open import univalent-combinatorics.standard-finite-types

Idea

Consider a family of types A indexed by Fin n. An n-ary correspondence of tuples (x₁, …, xₙ) where xᵢ : A i is a type family over (i : Fin n) → A i.

Definition

multivariable-correspondence :
  {l1 : Level} (l2 : Level) (n : ℕ) (A : Fin n → UU l1) → UU (l1 ⊔ lsuc l2)
multivariable-correspondence l2 n A = ((i : Fin n) → A i) → UU l2

Recent changes