{A : SuccStr} {P : ssFam A} (f g : ssForall P) := ssForall (ssfam_sshomotopy f g). Global Instance isgraph_ss : IsGraph SuccStr. Proof. snrapply Build_IsGraph. intros X Y. exact (@ssForall X (ssfam_const Y)). Defined.
Require Import Basics. Require Import Nat.Core. Require Import Spaces.Int. Require Import Spaces.Finite.Fin. Require Import WildCat.Core.