fact: Definition fracture_square (A : Type) : O_functor O2 (to O1 A) o to O2 A == to O2 (O1 A) o to O1 A := to_O_natural O2 (to O1 A).
imports: HoTT.Basics HoTT.Types Extensions Limits.Pullback Modality Lex Open Closed Nullification