Lemma θ_Strength1_int_implies_θ_Strength1 : θ_Strength1_int → θ_Strength1. Proof. unfold θ_Strength1_int, θ_Strength1. intros T X. assert (TX := T X). apply nat_trans_eq_alt. intro c; cbn. assert (T2 := nat_trans_eq_pointwise TX c). cbn in *. exact T2. Qed.
Require Import UniMath.Foundations.PartD. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.whiskering. Require Import UniMath.CategoryTheory.FunctorCategory. Require Import UniMath.CategoryTheory.PointedFunctors. Require Import UniMath.CategoryTheory.PrecategoryBinProduct. Require Import UniMath.CategoryTheory.HorizontalComposition. Require Import UniMath.CategoryTheory.BicatOfCatsElementary. Require Import UniMath.SubstitutionSystems.Notation.