Theorem TheoremOfHinzeAndWu : iscontr (∑ x : L μDD --> B, #L inDD · x = nat_trans_data_from_nat_trans σ μDD · # CC x · b). Proof. red. exists (traho_of_Hinze_Wu,, traho_of_Hinze_Wu_ok). intro t. induction t as [x hyp]. assert (same: x = traho_of_Hinze_Wu). 2: { apply subtypePath. + intro. simpl. apply C. + simpl. exact same. } etrans. { apply pathsinv0. apply (φ_adj_inv_after_φ_adj h). } etrans. 2: { apply (φ_adj_inv_after_φ_adj h). } apply maponpaths. unfold traho_of_Hinze_Wu. rewrite (φ_adj_after_φ_adj_inv h). apply φ_adj_h_x_equals_initial_arrow. simpl. etrans. { rewrite assoc. apply cancel_postcomposition. apply pathsinv0. apply hh. } etrans. { apply pathsinv0. apply φ_adj_natural_postcomp. } etrans. 2 : { apply φ_adj_natural_precomp. } apply maponpaths. apply pathsinv0. exact hyp. Defined.
Require Import UniMath.Foundations.Sets. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.whiskering. Require Import UniMath.CategoryTheory.FunctorAlgebras. Require Import UniMath.CategoryTheory.UnitorsAndAssociatorsForEndofunctors. Require Import UniMath.CategoryTheory.Limits.Initial. Require Import UniMath.CategoryTheory.Adjunctions.Core.