fact: Definition eta_path_arrow {A B : Type} (f g : A -> B) (p : f = g) : path_arrow f g (ap10 p) = p := eta_path_forall f g p.
imports: Basics.Overture Basics.PathGroupoids Basics.Decidable Basics.Equivalences Basics.Trunc Basics.Tactics Types.Forall