`{Univalence} {A} B n a b : ap (seq_colim_sum_to_sum_seq_colim B) (glue (sig_seq B) n (a;b)) = Delta _ (fib_seq_to_type_fam_beta_glue B n a) (inj _ _ _) @ ap (exist _ (inj A n a)) (glue (fib_seq_to_seq _ _) 0 b). Proof. srapply Colimit_rec_beta_colimp. Defined.
Require Import Basics. Require Import Types. Require Import Diagrams.Diagram. Require Import Diagrams.Sequence. Require Import Diagrams.Cocone. Require Import Colimits.Colimit. Require Import Spaces.Nat.Core. Require Import Homotopy.IdentitySystems.