Multivariable functoriality of set quotients
Content created by Fredrik Bakke, Egbert Rijke, Fernando Chu, Julian KG, fernabnor and louismntnu.
Created on 2023-03-26.
Last modified on 2023-06-25.
module foundation.multivariable-functoriality-set-quotients where
Imports
open import elementary-number-theory.natural-numbers open import foundation.functoriality-set-quotients open import foundation.set-quotients open import foundation.universe-levels open import foundation.vectors-set-quotients open import foundation-core.equivalence-relations open import foundation-core.function-types open import foundation-core.homotopies open import linear-algebra.vectors open import univalent-combinatorics.standard-finite-types
Idea
Say we have a family of types A1
, ..., An
each equipped with an equivalence
relation Ri
, as well as a type X
equipped with an equivalence relation S
,
Then, any multivariable operation from the Ai
s to the X
that respects the
equivalence relations extends uniquely to a multivariable operation from the
Ai/Ri
s to X/S
.
Definition
n-ary hom of equivalence relation
module _ { l1 l2 l3 l4 : Level} ( n : ℕ) ( A : functional-vec (UU l1) n) ( R : (i : Fin n) → Equivalence-Relation l2 (A i)) { X : UU l3} (S : Equivalence-Relation l4 X) where multivariable-map-set-quotient : ( h : hom-Equivalence-Relation (all-sim-Equivalence-Relation n A R) S) → set-quotient-vector n A R → set-quotient S multivariable-map-set-quotient = map-is-set-quotient ( all-sim-Equivalence-Relation n A R) ( set-quotient-vector-Set n A R) ( reflecting-map-quotient-vector-map n A R) ( S) ( quotient-Set S) ( reflecting-map-quotient-map S) ( is-set-quotient-vector-set-quotient n A R) ( is-set-quotient-set-quotient S) compute-multivariable-map-set-quotient : ( h : hom-Equivalence-Relation (all-sim-Equivalence-Relation n A R) S) → ( multivariable-map-set-quotient h ∘ quotient-vector-map n A R) ~ ( quotient-map S ∘ map-hom-Equivalence-Relation (all-sim-Equivalence-Relation n A R) S h) compute-multivariable-map-set-quotient = coherence-square-map-is-set-quotient ( all-sim-Equivalence-Relation n A R) ( set-quotient-vector-Set n A R) ( reflecting-map-quotient-vector-map n A R) ( S) ( quotient-Set S) ( reflecting-map-quotient-map S) ( is-set-quotient-vector-set-quotient n A R) ( is-set-quotient-set-quotient S)
Recent changes
- 2023-06-25. Fredrik Bakke, louismntnu, fernabnor, Egbert Rijke and Julian KG. Posets are categories, and refactor binary relations (#665).
- 2023-06-10. Egbert Rijke. cleaning up transport and dependent identifications files (#650).
- 2023-06-08. Fredrik Bakke. Remove empty
foundation
modules and replace them by their core counterparts (#644). - 2023-05-28. Fredrik Bakke. Enforce even indentation and automate some conventions (#635).
- 2023-05-01. Fredrik Bakke. Refactor 2, the sequel to refactor (#581).