forall x y, E (x;y). Proof. srapply (Colimit_ind _ F); intros n m p a; destruct p. exact ((I (fib_seq_to_type_fam_beta_glue B n a))^-1 (G n a)). 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.