proposition: Theorem TheoremOfHinzeAndWu : iscontr (∑ x : L μDD --> B, #L inDD · x = nat_trans_data_from_nat_trans σ μDD · # CC x · b).
proof: 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.
imports: UniMath.Foundations.Sets UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.whiskering UniMath.CategoryTheory.FunctorAlgebras UniMath.CategoryTheory.UnitorsAndAssociatorsForEndofunctors UniMath.CategoryTheory.Limits.Initial UniMath.CategoryTheory.Adjunctions.Core