FiniteSetProduct.v

Require Import UniMath.Combinatorics.FiniteSets.

Definition FiniteSetProduct (X Y : FiniteSet) : FiniteSet.
Proof.
  set (X' := pr1 X).           (* the underlying type of X *)
  set (X'_isfinite := pr2 X).  (* proof that X is a finite set *)
  set (Y' := pr1 Y).           (* the underlying type of Y *)
  set (Y'_isfinite := pr2 Y).  (* proof that Y is a finite set *)

  exists (X' × Y'). (* the underlying type for the product is the product of types *)

  use hinhfun.
  (* (X' × Y' is a finite set) is a proposition
     and we will be using propositions X'_isfinite and Y'_isfinite
     so we use hinhfun to "go under truncation"
   *)

  3: apply (hinhand X'_isfinite Y'_isfinite).
  (* here we just specify that we will be using
     a combination (product) of propositions X'_isfinite and Y'_isfinite *)

  intros P.  (* here P is untruncated version of X'_isfinite × Y'_isfinite *)

  set (n := pr1 (pr1 P) : nat). (* X has n elements *)
  set (X'_weq := pr2 (pr1 P) : (⟦n⟧)%stn ≃ X').
  (* equivalence with a standard finite set of size n *)

  set (m := pr1 (dirprod_pr2 P) : nat). (* Y has m elements *)
  set (Y'_weq := pr2 (dirprod_pr2 P) : (⟦m⟧)%stn ≃ Y').
  (* equivalence with a standard finite set of size m *)

  exists (n * m). (* product of finite sets has n * m elements *)
  eapply weqcomp. (* we will compose two equivalences together *)
  apply invweq, weqfromprodofstn. (* ⟦n * m⟧ ≃ ⟦n⟧ × ⟦m⟧ *)
  use weqdirprodf.
  - apply X'_weq. (* ⟦n⟧ ≃ X' *)
  - apply Y'_weq. (* ⟦m⟧ ≃ Y' *)
Defined.