fact: Definition make_is_cartesian_closed_bicat (B : bicat_with_binprod) (HB : is_univalent_2_1 B) (exp : B -> B → B) (app : ∏ (x y : B), exp x y ⊗ x --> y) (app2 : ∏ (x y₁ y₂ : B) (f g : y₁ --> exp x y₂) (α : f ⊗₁ id₁ x · app x y₂ ==> g ⊗₁ id₁ x · app x y₂), f ==> g) (app2_eq : ∏ (x y₁ y₂ : B) (f g : y₁ --> exp x y₂) (α : f ⊗₁ id₁ x · app x y₂ ==> g ⊗₁ id₁ x · app x y₂), app2 x y₁ y₂ f g α ⊗₂ id₂ (id₁ x) ▹ app x y₂ = α) (H : ∏ (x y₁ y₂ : B) (f g : y₁ --> exp x y₂) (α : f ⊗₁ id₁ x · app x y₂ ==> g ⊗₁ id₁ x · app x y₂) (β₁ β₂ : f ==> g) (p₁ : β₁ ⊗₂ id₂ (id₁ x) ▹ app x y₂ = α) (p₂ : β₂ ⊗₂ id₂ (id₁ x) ▹ app x y₂ = α), β₁ = β₂) (lam : ∏ (x y₁ y₂ : B) (f : y₁ ⊗ x --> y₂), y₁ --> exp x y₂) (app_lam : ∏ (x y₁ y₂ : B) (f : y₁ ⊗ x --> y₂), invertible_2cell (lam x y₁ y₂ f ⊗₁ id₁ x · app x y₂) f) : is_cartesian_closed_bicat B.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.Bicategories.Core.Bicat UniMath.Bicategories.Core.Invertible_2cells UniMath.Bicategories.Core.Univalence UniMath.Bicategories.Core.BicategoryLaws UniMath.Bicategories.Core.Unitors UniMath.Bicategories.DisplayedBicats.DispBicat UniMath.Bicategories.DisplayedBicats.Examples.Slice UniMath.Bicategories.Limits.Products UniMath.Bicategories.Limits.Pullbacks UniMath.Bicategories.Limits.PullbackFunctions UniMath.Bicategories.Morphisms.InternalStreetFibration UniMath.Bicategories.Morphisms.InternalStreetOpFibration UniMath.Bicategories.PseudoFunctors.Display.PseudoFunctorBicat UniMath.Bicategories.PseudoFunctors.PseudoFunctor UniMath.Bicategories.PseudoFunctors.UniversalArrow UniMath.Bicategories.PseudoFunctors.Examples.ConstProduct UniMath.Bicategories.PseudoFunctors.Examples.PullbackFunctor