Could not find an instance for "IsColimit@{HoTT.Homotopy.JoinConstruction.1231 k k k HoTT.Homotopy.JoinConstruction.1224 HoTT.Homotopy.JoinConstruction.1225 HoTT.Homotopy.JoinConstruction.1231} s (Colimit@{u u u u u u u} s')" in environment: H : Funext s : Sequence@{k k k} ss : forall n : Graph.graph0@{k k} sequence_graph@{k k}, IsSmall@{u k} (s n) s' := Build_Sequence@{u u u} (fun n : nat => smalltype@{u k} (s n)) ((fun (n : nat) (x : smalltype@{u k} (s n)) => (equiv_smalltype@{u k} (s n.+1%nat))^-1 (sequence_arr@{k k k} s n (equiv_smalltype@{u k} (s n) x))) : forall n : nat, (fun n0 : nat => smalltype@{u k} (s n0)) n -> (fun n0 : nat => smalltype@{u k} (s n0)) n.+1%nat) : Sequence@{u u u} Command exited with non-zero status 1