`{Univalence} (k : trunc_index) {N : SuccStr} (S : LongExactSequence purely N) : LongExactSequence (Tr k) N := Build_LongExactSequence (Tr k) N (fun n => pTr k.
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.