(F X Y : pType) (n : N3) : pType := match n with | (n, inl (inl (inl x))) => Empty_ind _ x | (n, inl (inl (inr tt))) => iterated_loops n Y | (n, inl (inr tt)) => iterated_loops n X | (n, inr tt) => iterated_loops n F end.
Require Import Basics Types. Require Import SuccessorStructure. Require Import WildCat. Require Import Pointed. Require Import Modalities.Identity Modalities.Descent. Require Import Truncations. Require Import HFiber. Require Import ObjectClassifier.