{n : trunc_index} {X Y : Type} (f : X -> Y) `{MapIn (Tr n.+1) _ _ f} (pc : PlusConnMap L O f) : MapIn (Tr n) (plus_functor L O f). Proof. generalize dependent f; revert X Y; induction n as [|n IHn]; intros X Y f ? pc. { apply mapinO_tr_istruncmap, contr_map_isequiv, composing; assumption. } pose (O_eq_Tr n). apply (mapinO_O_leq (Sep (Tr n)) _), mapinO_from_diagonal. nrapply (mapinO_homotopic (Tr n) _ (fun u => (diagonal_plus_functor f u)^)). apply mapinO_compose. 2:rapply mapinO_isequiv. apply IHn. - rapply mapinO_diagonal. pose (O_eq_Tr n.+1). rapply (mapinO_O_leq _ (Sep (Tr n.+1))). - apply plusconnmap_diagonal; assumption. Defined.
Require Import HoTT.Basics HoTT.Types. Require Import Extensions HFiber Truncations NullHomotopy Limits.Pullback. Require Import Descent Lex Separated.