fact: Record diagram_equiv (D1 D2: Diagram G) := { diag_equiv_map :> DiagramMap D1 D2; diag_equiv_isequiv : forall i, IsEquiv (diag_equiv_map i) }.
imports: Basics Types HoTT.Tactics Diagrams.CommutativeSquares Diagrams.Graph