fact: Record DiagramMap (D1 D2 : Diagram G) := { DiagramMap_obj :> forall i, D1 i -> D2 i; DiagramMap_comm : forall i j (g: G i j) x, D2 _f g (DiagramMap_obj i x) = DiagramMap_obj j (D1 _f g x) }.
imports: Basics Types HoTT.Tactics Diagrams.CommutativeSquares Diagrams.Graph