# Cartesian products of set quotients

Content created by Fredrik Bakke, Egbert Rijke, Daniel Gratzer, Elisabeth Stenholm, Fernando Chu, Julian KG, fernabnor and louismntnu.

Created on 2023-03-26.

module foundation.cartesian-products-set-quotients where

Imports
open import foundation.action-on-identifications-functions
open import foundation.dependent-pair-types
open import foundation.equality-cartesian-product-types
open import foundation.function-extensionality
open import foundation.products-equivalence-relations
open import foundation.reflecting-maps-equivalence-relations
open import foundation.set-quotients
open import foundation.sets
open import foundation.uniqueness-set-quotients
open import foundation.universal-property-set-quotients
open import foundation.universe-levels

open import foundation-core.cartesian-product-types
open import foundation-core.equality-dependent-pair-types
open import foundation-core.equivalence-relations
open import foundation-core.equivalences
open import foundation-core.function-types
open import foundation-core.homotopies
open import foundation-core.identity-types
open import foundation-core.propositions


## Idea

Given two types A and B, equipped with equivalence relations R and S, respectively, the cartesian product of their set quotients is the set quotient of their product.

## Definition

### The product of two relations

module _
{l1 l2 l3 l4 : Level}
{A : UU l1} (R : equivalence-relation l2 A)
{B : UU l3} (S : equivalence-relation l4 B)
where

product-set-quotient-Set : Set (l1 ⊔ l2 ⊔ l3 ⊔ l4)
product-set-quotient-Set = product-Set (quotient-Set R) (quotient-Set S)

product-set-quotient : UU (l1 ⊔ l2 ⊔ l3 ⊔ l4)
product-set-quotient = pr1 product-set-quotient-Set

is-set-product-set-quotient : is-set product-set-quotient
is-set-product-set-quotient = pr2 product-set-quotient-Set

product-set-quotient-map : (A × B) → product-set-quotient
product-set-quotient-map (a , b) =
pair (quotient-map R a) (quotient-map S b)

reflecting-map-product-quotient-map :
reflecting-map-equivalence-relation
( product-equivalence-relation R S)
( product-set-quotient)
reflecting-map-product-quotient-map =
pair
product-set-quotient-map
( λ (p , q) →
( eq-pair
( apply-effectiveness-quotient-map' R p)
( apply-effectiveness-quotient-map' S q)))


## Properties

### The product of sets quotients is a set quotient

  inv-precomp-set-quotient-product-set-quotient :
{l : Level}
(X : Set l) →
reflecting-map-equivalence-relation
( product-equivalence-relation R S)
( type-Set X) →
hom-Set product-set-quotient-Set X
inv-precomp-set-quotient-product-set-quotient X (f , H) (qa , qb) =
inv-precomp-set-quotient
( R)
( hom-set-Set (quotient-Set S) X)
( pair
( λ a qb' →
inv-precomp-set-quotient S X
( pair
(λ b → f (a , b))
(λ p → H (refl-equivalence-relation R a , p)))
qb')
( λ {a1} {a2} p →
( ap (inv-precomp-set-quotient S X)
( eq-pair-Σ
( eq-htpy (λ b → H (p , refl-equivalence-relation S b)))
( eq-is-prop
( is-prop-reflects-equivalence-relation S X _))))))
( qa)
( qb)

is-section-inv-precomp-set-quotient-product-set-quotient :
{ l : Level}
( X : Set l) →
( precomp-Set-Quotient
( product-equivalence-relation R S)
( product-set-quotient-Set)
( reflecting-map-product-quotient-map)
( X) ∘
( inv-precomp-set-quotient-product-set-quotient X)) ~
( id)
is-section-inv-precomp-set-quotient-product-set-quotient X (f , H) =
eq-pair-Σ
( eq-htpy
( λ (a , b) →
( htpy-eq
( is-section-inv-precomp-set-quotient R
( hom-set-Set (quotient-Set S) X) _ a)
( quotient-map S b) ∙
( is-section-inv-precomp-set-quotient S X _ b))))
( eq-is-prop
( is-prop-reflects-equivalence-relation
( product-equivalence-relation R S) X f))

is-retraction-inv-precomp-set-quotient-product-set-quotient :
{ l : Level}
( X : Set l) →
( ( inv-precomp-set-quotient-product-set-quotient X) ∘
( precomp-Set-Quotient
( product-equivalence-relation R S)
( product-set-quotient-Set)
( reflecting-map-product-quotient-map)
( X))) ~
( id)
is-retraction-inv-precomp-set-quotient-product-set-quotient X f =
( eq-htpy
( λ (qa , qb) →
htpy-eq
( htpy-eq
( ap
( inv-precomp-set-quotient
( R)
( hom-set-Set (quotient-Set S) X))
( eq-pair-Σ
( eq-htpy λ a →
( ap
( inv-precomp-set-quotient S X)
( eq-pair-eq-fiber
( eq-is-prop
( is-prop-reflects-equivalence-relation S X _)))) ∙
( is-retraction-inv-precomp-set-quotient S X _))
( eq-is-prop
( is-prop-reflects-equivalence-relation R
( hom-set-Set (quotient-Set S) X) _))) ∙
( is-retraction-inv-precomp-set-quotient R
( hom-set-Set (quotient-Set S) X)
( λ qa qb → f (qa , qb))))
( qa))
( qb)))

is-set-quotient-product-set-quotient :
is-set-quotient
( product-equivalence-relation R S)
( product-set-quotient-Set)
( reflecting-map-product-quotient-map)
pr1 (pr1 (is-set-quotient-product-set-quotient X)) =
inv-precomp-set-quotient-product-set-quotient X
pr2 (pr1 (is-set-quotient-product-set-quotient X)) =
is-section-inv-precomp-set-quotient-product-set-quotient X
pr1 (pr2 (is-set-quotient-product-set-quotient X)) =
inv-precomp-set-quotient-product-set-quotient X
pr2 (pr2 (is-set-quotient-product-set-quotient X)) =
is-retraction-inv-precomp-set-quotient-product-set-quotient X

quotient-product : Set (l1 ⊔ l2 ⊔ l3 ⊔ l4)
quotient-product = quotient-Set (product-equivalence-relation R S)

type-quotient-product : UU (l1 ⊔ l2 ⊔ l3 ⊔ l4)
type-quotient-product = pr1 quotient-product

equiv-quotient-product-product-set-quotient :
product-set-quotient ≃ type-Set (quotient-product)
equiv-quotient-product-product-set-quotient =
equiv-uniqueness-set-quotient
( product-equivalence-relation R S)
( product-set-quotient-Set)
( reflecting-map-product-quotient-map)
( is-set-quotient-product-set-quotient)
( quotient-product)
( reflecting-map-quotient-map (product-equivalence-relation R S))
( is-set-quotient-set-quotient (product-equivalence-relation R S))

triangle-uniqueness-product-set-quotient :
( map-equiv equiv-quotient-product-product-set-quotient ∘
product-set-quotient-map) ~
quotient-map (product-equivalence-relation R S)
triangle-uniqueness-product-set-quotient =
triangle-uniqueness-set-quotient
( product-equivalence-relation R S)
( product-set-quotient-Set)
( reflecting-map-product-quotient-map)
( is-set-quotient-product-set-quotient)
( quotient-product)
( reflecting-map-quotient-map (product-equivalence-relation R S))
( is-set-quotient-set-quotient (product-equivalence-relation R S))