# Cartesian products of finite types ```agda module univalent-combinatorics.cartesian-product-types where ``` <details><summary>Imports</summary> ```agda 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 ``` </details> ## 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 ```agda 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) ``` ```agda 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 ``` ```agda 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)) ``` ```agda 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)))) ```