fact: Definition limit_up_weq {X L} {C : cone d L} {is : is_limit_cone C} : (X → L) ≃ cone d X := make_weq (into_cone_to_cone C) (is X).
imports: UniMath.Foundations.PartD UniMath.Foundations.Sets UniMath.MoreFoundations.Univalence UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Categories.Type.Core UniMath.CategoryTheory.Limits.Graphs.Limits UniMath.CategoryTheory.Limits.Graphs.Colimits UniMath.CategoryTheory.Chains.Cochains