{X Y} : Tr n (X * Y) <~> Tr n X * Tr n Y := equiv_O_prod_cmp (Tr n) X Y. Global Instance is1functor_Tr : Is1Functor (Tr n). Proof. apply Build_Is1Functor. - apply @O_functor_homotopy. - apply @Trunc_functor_idmap. - apply @Trunc_functor_compose. Defined.
Require Import Basics Types WildCat.Core WildCat.Universe HFiber. Require Import Modalities.Modality.