s : morphism s s. Proof. exists 1. apply identity_H. Defined.
Require Import Category.Core Functor.Core. Require Import SetCategory.Core. Require Import Basics.Trunc Types.Sigma. Require Import Basics.Tactics.