# Cartesian products of finite types

Content created by Fredrik Bakke, Egbert Rijke, Jonathan Prieto-Cubides, Elisabeth Stenholm and Victor Blanchi.

Created on 2022-03-14.

module univalent-combinatorics.cartesian-product-types where

Imports
open import elementary-number-theory.multiplication-natural-numbers
open import elementary-number-theory.natural-numbers

open import foundation.cartesian-product-types
open import foundation.contractible-types
open import foundation.decidable-equality
open import foundation.dependent-pair-types
open import foundation.equivalences
open import foundation.function-types
open import foundation.functoriality-cartesian-product-types
open import foundation.functoriality-coproduct-types
open import foundation.functoriality-dependent-pair-types
open import foundation.functoriality-propositional-truncation
open import foundation.identity-types
open import foundation.mere-equivalences
open import foundation.propositional-truncations
open import foundation.torsorial-type-families
open import foundation.type-arithmetic-cartesian-product-types
open import foundation.type-arithmetic-coproduct-types
open import foundation.type-arithmetic-dependent-pair-types
open import foundation.type-arithmetic-empty-type
open import foundation.type-arithmetic-unit-type
open import foundation.unit-type
open import foundation.universe-levels

open import univalent-combinatorics.coproduct-types
open import univalent-combinatorics.counting
open import univalent-combinatorics.counting-dependent-pair-types
open import univalent-combinatorics.decidable-propositions
open import univalent-combinatorics.double-counting
open import univalent-combinatorics.finite-types
open import univalent-combinatorics.standard-finite-types


## Idea

The cartesian product of finite types is finite. We obtain a cartesian product operation on finite types.

### The standard finite types are closed under cartesian products

product-Fin : (k l : ℕ) → ((Fin k) × (Fin l)) ≃ Fin (k *ℕ l)
product-Fin zero-ℕ l = left-absorption-product (Fin l)
product-Fin (succ-ℕ k) l =
( ( coproduct-Fin (k *ℕ l) l) ∘e
( equiv-coproduct (product-Fin k l) left-unit-law-product)) ∘e
( right-distributive-product-coproduct (Fin k) unit (Fin l))

Fin-mul-ℕ : (k l : ℕ) → (Fin (k *ℕ l)) ≃ ((Fin k) × (Fin l))
Fin-mul-ℕ k l = inv-equiv (product-Fin k l)

count-product :
{l1 l2 : Level} {X : UU l1} {Y : UU l2} → count X → count Y → count (X × Y)
pr1 (count-product (pair k e) (pair l f)) = k *ℕ l
pr2 (count-product (pair k e) (pair l f)) =
(equiv-product e f) ∘e (inv-equiv (product-Fin k l))

abstract
number-of-elements-count-product :
{l1 l2 : Level} {A : UU l1} {B : UU l2} (count-A : count A)
(count-B : count B) →
Id
( number-of-elements-count
( count-product count-A count-B))
( ( number-of-elements-count count-A) *ℕ
( number-of-elements-count count-B))
number-of-elements-count-product (pair k e) (pair l f) = refl

equiv-left-factor :
{l1 l2 : Level} {X : UU l1} {Y : UU l2} (y : Y) →
(Σ (X × Y) (λ t → Id (pr2 t) y)) ≃ X
equiv-left-factor {l1} {l2} {X} {Y} y =
( ( right-unit-law-product) ∘e
( equiv-tot
( λ x → equiv-is-contr (is-torsorial-Id' y) is-contr-unit))) ∘e
( associative-Σ X (λ x → Y) (λ t → Id (pr2 t) y))

count-left-factor :
{l1 l2 : Level} {X : UU l1} {Y : UU l2} → count (X × Y) → Y → count X
count-left-factor e y =
count-equiv
( equiv-left-factor y)
( count-Σ e
( λ z →
count-eq
( has-decidable-equality-right-factor
( has-decidable-equality-count e)
( pr1 z))
( pr2 z)
( y)))

count-right-factor :
{l1 l2 : Level} {X : UU l1} {Y : UU l2} → count (X × Y) → X → count Y
count-right-factor e x =
count-left-factor (count-equiv commutative-product e) x

abstract
product-number-of-elements-product :
{l1 l2 : Level} {A : UU l1} {B : UU l2} (count-AB : count (A × B)) →
(a : A) (b : B) →
Id
( ( number-of-elements-count (count-left-factor count-AB b)) *ℕ
( number-of-elements-count (count-right-factor count-AB a)))
( number-of-elements-count count-AB)
product-number-of-elements-product count-AB a b =
( inv
( number-of-elements-count-product
( count-left-factor count-AB b)
( count-right-factor count-AB a))) ∙
( double-counting
( count-product
( count-left-factor count-AB b)
( count-right-factor count-AB a))
( count-AB))

abstract
is-finite-product :
{l1 l2 : Level} {X : UU l1} {Y : UU l2} →
is-finite X → is-finite Y → is-finite (X × Y)
is-finite-product {X = X} {Y} is-finite-X is-finite-Y =
apply-universal-property-trunc-Prop is-finite-X
( is-finite-Prop (X × Y))
( λ (e : count X) →
apply-universal-property-trunc-Prop is-finite-Y
( is-finite-Prop (X × Y))
( is-finite-count ∘ (count-product e)))

product-𝔽 : {l1 l2 : Level} → 𝔽 l1 → 𝔽 l2 → 𝔽 (l1 ⊔ l2)
pr1 (product-𝔽 X Y) = (type-𝔽 X) × (type-𝔽 Y)
pr2 (product-𝔽 X Y) =
is-finite-product (is-finite-type-𝔽 X) (is-finite-type-𝔽 Y)

abstract
is-finite-left-factor :
{l1 l2 : Level} {X : UU l1} {Y : UU l2} →
is-finite (X × Y) → Y → is-finite X
is-finite-left-factor f y =
map-trunc-Prop (λ e → count-left-factor e y) f

abstract
is-finite-right-factor :
{l1 l2 : Level} {X : UU l1} {Y : UU l2} →
is-finite (X × Y) → X → is-finite Y
is-finite-right-factor f x =
map-trunc-Prop (λ e → count-right-factor e x) f

product-UU-Fin :
{l1 l2 : Level} (k l : ℕ) → UU-Fin l1 k → UU-Fin l2 l →
UU-Fin (l1 ⊔ l2) (k *ℕ l)
pr1 (product-UU-Fin k l (pair X H) (pair Y K)) = X × Y
pr2 (product-UU-Fin k l (pair X H) (pair Y K)) =
apply-universal-property-trunc-Prop H
( mere-equiv-Prop (Fin (k *ℕ l)) (X × Y))
( λ e1 →
apply-universal-property-trunc-Prop K
( mere-equiv-Prop (Fin (k *ℕ l)) (X × Y))
( λ e2 →
unit-trunc-Prop (equiv-product e1 e2 ∘e inv-equiv (product-Fin k l))))