{T0} `{IsHSet T0} (a b : T0) (pf : a = b) : Contr (b = a). Proof. destruct pf. apply contr_inhabited_hprop; try reflexivity. typeclasses eauto. 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.