Definition precatDelta : precategory . Proof. use tpair. { use tpair. { exists nat. intros m n. exact (monfunstn (S m) (S n)). } { split. { intros m. apply monfunstnid. } { intros l m n f g. exact (monfunstncomp f g). } } } apply is_precategory_one_assoc_to_two. simpl. split. { simpl. split. { intros m n f. now apply monfunstnpr1_isInjective. } { intros m n f. now apply monfunstnpr1_isInjective. } } { simpl. intros m n o p f g h. now apply monfunstnpr1_isInjective. } Defined.
Require Import UniMath.MoreFoundations.Tactics.