ap_b_path_object' x y Ha Hb Hf : ap (@b) (@path_object' x y Ha Hb Hf) = Hb. Proof. destruct x, y; simpl in *. destruct Ha, Hb, Hf; simpl in *. reflexivity. Qed.
Require Import HoTT.Basics HoTT.Types. Require Import Functor.Core. Require Import InitialTerminalCategory.Core InitialTerminalCategory.Functors. Require Import Category.Strict. Import Functor.Identity.FunctorIdentityNotations. Module Import CommaCategory.