fact: Definition ooextendable_compose {A B C : Type} (P : C -> Type) (f : A -> B) (g : B -> C) : ooExtendableAlong g P -> ooExtendableAlong f (fun b => P (g b)) -> ooExtendableAlong (g o f) P := fun extg extf n => extendable_compose n P f g (extg n) (extf n).
imports: HoTT.Basics HoTT.Types Equiv.PathSplit PathAny Cubical.DPath Cubical.DPathSquare Colimits.Coeq Colimits.MappingCylinder