{A} {P : A -> Type} {a00 b00} : DPathSquare P sq_id 1 1 1 1 (a00:=a00) (b00:=b00). Proof. apply sq_id. Defined.
Require Import Basics. Require Import Types.Paths. Require Import Cubical.DPath. Require Import Cubical.PathSquare.