pi_prod' {n : nat} (X Y : pType) : pPi n (X * Y) <~>* (pPi n X) * (pPi n Y). Proof. refine (_ o*E pequiv_ppi_ptr_iterated_loops _ _). refine ((equiv_functor_pprod (pequiv_ppi_ptr_iterated_loops _ _) (pequiv_ppi_ptr_iterated_loops _ _))^-1* o*E _). refine (_ o*E pequiv_ptr_functor 0 _). 1: nrapply iterated_loops_prod. snrapply Build_pEquiv'; cbn. - refine (equiv_O_prod_cmp 0 _ _). - reflexivity. Defined.
Require Import Basics Types Pointed HSet. Require Import Modalities.Modality. Require Import Truncations.Core Truncations.SeparatedTrunc. Require Import Algebra.AbGroups. Require Import WildCat.