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
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
Recent changes
- 2023-06-08. Fredrik Bakke. Remove empty
foundation
modules and replace them by their core counterparts (#644). - 2023-03-14. Fredrik Bakke. Remove all unused imports (#502).
- 2023-03-13. Jonathan Prieto-Cubides. More maintenance (#506).
- 2023-03-10. Fredrik Bakke. Additions to
fix-import
(#497). - 2023-03-09. Jonathan Prieto-Cubides. Add hooks (#495).