fact: Definition loops_carrier (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.
imports: Basics Types SuccessorStructure WildCat Pointed Modalities.Identity Modalities.Descent Truncations HFiber ObjectClassifier