A : IsPullback (fracture_square A). Proof. apply ispullback_symm. nrefine (ispullback_connmap_mapino_commsq O2 _). 1-3:exact _. 2:rapply mapinO_between_inO. intros x; refine (ino2_isconnectedo1 _ _). Defined.
Require Import HoTT.Basics HoTT.Types. Require Import Extensions Limits.Pullback. Require Import Modality Lex Open Closed Nullification.