(G : Graph) := { obj : G -> Type; arr {i j : G} : G i j -> obj i -> obj j }.
Require Import Basics. Require Import Types. Require Import HoTT.Tactics. Require Import Diagrams.CommutativeSquares. Require Import Diagrams.Graph.