s d d' (m1 : morphism d d') (m2 : morphism s d) : (F _1 (m1 .1 o m2 .1)) s.(x) = d'.(x). Proof. etransitivity; [ | exact (m1.2) ]. etransitivity; [ | apply ap; exact (m2.2) ]. match goal with | [ |- ?f ?x = ?g (?h ?x) ] => change (f x = (g o h) x) end. match goal with | [ |- ?f ?x = ?g ?x ] => apply (@apD10 _ _ f g) end. apply (composition_of F). Defined.
Require Import Category.Core Functor.Core. Require Import SetCategory.Core. Require Import Basics.Trunc Types.Sigma. Require Import Basics.Tactics.