fact: Definition path_arrow_1 {A B : Type} (f : A -> B) : (path_arrow f f (fun x => 1)) = 1 := eta_path_arrow f f 1.
imports: Basics.Overture Basics.PathGroupoids Basics.Decidable Basics.Equivalences Basics.Trunc Basics.Tactics Types.Forall