This is an archived version pinned as of the submission of my master's thesis. An up-to-date version may be found online.

Multivariable correspondences

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_n) where x_i : 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