Multivariable correspondences

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

Created on 2022-09-09.
Last modified on 2023-06-08.

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

open import foundation.universe-levels

open import univalent-combinatorics.standard-finite-types


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


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