ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>I : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} I<VAR>B : Type u₂<VAR>CategoryTheory.Bicategory B<VAR>CategoryTheory.Bicategory.Strict B<VAR>F : CategoryTheory.Functor I B<GOAL>∀ {a b : CategoryTheory.LocallyDiscrete I} {f g : a ⟶ b} (η : f ⟶ g), F.toPseudoFunctor.map₂ η = CategoryTheory.eqToHom ⋯
<VAR>I : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} I<VAR>B : Type u₂<VAR>CategoryTheory.Bicategory B<VAR>CategoryTheory.Bicategory.Strict B<VAR>F : CategoryTheory.Functor I B<GOAL>∀ {X Y : CategoryTheory.LocallyDiscrete I} (f : X ⟶ Y), F.toPseudoFunctor.map f = F.map f.as
<VAR>I : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} I<VAR>B : Type u₂<VAR>CategoryTheory.Bicategory B<VAR>CategoryTheory.Bicategory.Strict B<VAR>F : CategoryTheory.Functor I B<VAR>i : CategoryTheory.LocallyDiscrete I<GOAL>F.toPseudoFunctor.mapId i = CategoryTheory.eqToIso ⋯
<VAR>I : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} I<VAR>B : Type u₂<VAR>CategoryTheory.Bicategory B<VAR>CategoryTheory.Bicategory.Strict B<VAR>F : CategoryTheory.Functor I B<GOAL>∀ {a b c : CategoryTheory.LocallyDiscrete I} (f : a ⟶ b) (g : b ⟶ c), F.toPseudoFunctor.mapComp f g = CategoryTheory.eqToIso ⋯
<VAR>I : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} I<VAR>B : Type u₂<VAR>CategoryTheory.Bicategory B<VAR>CategoryTheory.Bicategory.Strict B<VAR>F : CategoryTheory.Functor I B<VAR>i : CategoryTheory.LocallyDiscrete I<GOAL>F.toPseudoFunctor.obj i = F.obj i.as
<VAR>I : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} I<VAR>B : Type u₂<VAR>CategoryTheory.Bicategory B<VAR>CategoryTheory.Bicategory.Strict B<VAR>F : CategoryTheory.Functor I B<GOAL>∀ {a b : CategoryTheory.LocallyDiscrete I} {f g : a ⟶ b} (η : f ⟶ g), F.toOplaxFunctor.map₂ η = CategoryTheory.eqToHom ⋯
<VAR>I : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} I<VAR>B : Type u₂<VAR>CategoryTheory.Bicategory B<VAR>CategoryTheory.Bicategory.Strict B<VAR>F : CategoryTheory.Functor I B<VAR>i : CategoryTheory.LocallyDiscrete I<GOAL>F.toOplaxFunctor.obj i = F.obj i.as
<VAR>I : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} I<VAR>B : Type u₂<VAR>CategoryTheory.Bicategory B<VAR>CategoryTheory.Bicategory.Strict B<VAR>F : CategoryTheory.Functor I B<VAR>i : CategoryTheory.LocallyDiscrete I<GOAL>F.toOplaxFunctor.mapId i = CategoryTheory.eqToHom ⋯
<VAR>I : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} I<VAR>B : Type u₂<VAR>CategoryTheory.Bicategory B<VAR>CategoryTheory.Bicategory.Strict B<VAR>F : CategoryTheory.Functor I B<GOAL>∀ {a b c : CategoryTheory.LocallyDiscrete I} (f : a ⟶ b) (g : b ⟶ c), F.toOplaxFunctor.mapComp f g = CategoryTheory.eqToHom ⋯
<VAR>I : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} I<VAR>B : Type u₂<VAR>CategoryTheory.Bicategory B<VAR>CategoryTheory.Bicategory.Strict B<VAR>F : CategoryTheory.Functor I B<GOAL>∀ {X Y : CategoryTheory.LocallyDiscrete I} (f : X ⟶ Y), F.toOplaxFunctor.map f = F.map f.as
<VAR>B : Type u₁<VAR>CategoryTheory.Bicategory B<VAR>C : Type u₂<VAR>CategoryTheory.Bicategory C<VAR>F : CategoryTheory.PrelaxFunctor B C<VAR>a b : B<VAR>f g : a ⟶ b<VAR>h : f = g<GOAL>F.map₂ (CategoryTheory.eqToHom h) = CategoryTheory.eqToHom ⋯
<VAR>C : Type u<VAR>CategoryTheory.CategoryStruct.{v, u} C<VAR>a b : C<VAR>f : a ⟶ b<GOAL>f.toLoc.as = f
<VAR>C : Type u<VAR>CategoryTheory.CategoryStruct.{v, u} C<VAR>a : C<GOAL>(CategoryTheory.CategoryStruct.id a).toLoc = CategoryTheory.CategoryStruct.id { as := a }
<VAR>C : Type u<VAR>CategoryTheory.CategoryStruct.{v, u} C<VAR>a b c : C<VAR>f : a ⟶ b<VAR>g : b ⟶ c<GOAL>(CategoryTheory.CategoryStruct.comp f g).toLoc = CategoryTheory.CategoryStruct.comp f.toLoc g.toLoc
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>a b : C<VAR>h : a = b<GOAL>(CategoryTheory.eqToHom h).toLoc = CategoryTheory.eqToHom ⋯
<VAR>c : Type u → Type u<VAR>hom : ⦃α β : Type u⦄ → c α → c β → (α → β) → Prop<VAR>self : CategoryTheory.UnbundledHom hom<VAR>α β γ : Type u<VAR>Iα : c α<VAR>Iβ : c β<VAR>Iγ : c γ<VAR>g : β → γ<VAR>f : α → β<GOAL>hom Iβ Iγ g → hom Iα Iβ f → hom Iα Iγ (g ∘ f)
<VAR>c : Type u → Type u<VAR>hom : ⦃α β : Type u⦄ → c α → c β → (α → β) → Prop<VAR>self : CategoryTheory.UnbundledHom hom<VAR>α : Type u<VAR>ia : c α<GOAL>hom ia ia id
<VAR>B : Type u<VAR>CategoryTheory.Bicategory B<VAR>a b c : B<VAR>f : a ⟶ b<VAR>g : a ⟶ c<VAR>s t : CategoryTheory.Bicategory.LeftExtension f g<VAR>η : s ⟶ t<GOAL>CategoryTheory.CategoryStruct.comp s.unit (CategoryTheory.Bicategory.whiskerLeft f η.right) = t.unit
<VAR>B : Type u<VAR>CategoryTheory.Bicategory B<VAR>a b c : B<VAR>f : a ⟶ b<VAR>g : a ⟶ c<VAR>t : CategoryTheory.Bicategory.LeftExtension f (CategoryTheory.CategoryStruct.comp g (CategoryTheory.CategoryStruct.id c))<GOAL>t.ofCompId.right = t.extension
<VAR>B : Type u<VAR>CategoryTheory.Bicategory B<VAR>a b c : B<VAR>f : a ⟶ b<VAR>g : a ⟶ c<VAR>t : CategoryTheory.Bicategory.LeftExtension f (CategoryTheory.CategoryStruct.comp g (CategoryTheory.CategoryStruct.id c))<GOAL>t.ofCompId.hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.rightUnitor g).inv t.unit
<VAR>B : Type u<VAR>CategoryTheory.Bicategory B<VAR>a b c : B<VAR>f : a ⟶ b<VAR>g : a ⟶ c<VAR>t : CategoryTheory.Bicategory.LeftExtension f (CategoryTheory.CategoryStruct.comp g (CategoryTheory.CategoryStruct.id c))<GOAL>t.ofCompId.left.as = PUnit.unit
<VAR>B : Type u<VAR>CategoryTheory.Bicategory B<VAR>a b c : B<VAR>f : a ⟶ b<VAR>g : a ⟶ c<VAR>t : CategoryTheory.Bicategory.LeftExtension f g<VAR>x : B<VAR>h : c ⟶ x<GOAL>(t.whisker h).extension = CategoryTheory.CategoryStruct.comp t.extension h
<VAR>B : Type u<VAR>CategoryTheory.Bicategory B<VAR>a b c : B<VAR>f : a ⟶ b<VAR>g : a ⟶ c<VAR>t : CategoryTheory.Bicategory.LeftExtension f g<VAR>x : B<VAR>h : c ⟶ x<GOAL>(t.whisker h).unit = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight t.unit h) (CategoryTheory.Bicategory.associator f t.extension h).hom
<VAR>B : Type u<VAR>CategoryTheory.Bicategory B<VAR>a b c : B<VAR>f : a ⟶ b<VAR>g : a ⟶ c<VAR>x : B<VAR>h : c ⟶ x<VAR>t : CategoryTheory.Bicategory.LeftExtension f g<GOAL>(CategoryTheory.Bicategory.LeftExtension.whiskering h).obj t = t.whisker h
<VAR>B : Type u<VAR>CategoryTheory.Bicategory B<VAR>a b c : B<VAR>f : a ⟶ b<VAR>g : a ⟶ c<VAR>x : B<VAR>h : c ⟶ x<GOAL>∀ {X Y : CategoryTheory.Bicategory.LeftExtension f g} (η : X ⟶ Y), (CategoryTheory.Bicategory.LeftExtension.whiskering h).map η = CategoryTheory.Bicategory.LeftExtension.homMk (CategoryTheory.Bicategory.whiskerRight η.right h) ⋯
<VAR>B : Type u<VAR>CategoryTheory.Bicategory B<VAR>a b c : B<VAR>f : a ⟶ b<VAR>g : a ⟶ c<VAR>s : CategoryTheory.Bicategory.LeftExtension f (CategoryTheory.CategoryStruct.comp g (CategoryTheory.CategoryStruct.id c))<VAR>t : CategoryTheory.Bicategory.LeftExtension f g<VAR>τ : s ⟶ t.whisker (CategoryTheory.CategoryStruct.id c)<GOAL>(s.whiskerIdCancel τ).right = CategoryTheory.CategoryStruct.comp τ.right (CategoryTheory.Bicategory.rightUnitor t.extension).hom
<VAR>B : Type u<VAR>CategoryTheory.Bicategory B<VAR>a b c : B<VAR>f : a ⟶ b<VAR>g : a ⟶ c<VAR>s t : CategoryTheory.Bicategory.LeftExtension f g<VAR>i : s ⟶ t<VAR>x : B<VAR>h : c ⟶ x<GOAL>(CategoryTheory.Bicategory.LeftExtension.whiskerHom i h).right = CategoryTheory.Bicategory.whiskerRight i.right h
<VAR>B : Type u<VAR>CategoryTheory.Bicategory B<VAR>a b c : B<VAR>f : a ⟶ b<VAR>g : a ⟶ c<VAR>t : CategoryTheory.Bicategory.LeftExtension f g<GOAL>t.whiskerOfCompIdIsoSelf.inv.right = (CategoryTheory.Bicategory.rightUnitor t.extension).inv
<VAR>B : Type u<VAR>CategoryTheory.Bicategory B<VAR>a b c : B<VAR>f : a ⟶ b<VAR>g : a ⟶ c<VAR>t : CategoryTheory.Bicategory.LeftExtension f g<GOAL>t.whiskerOfCompIdIsoSelf.hom.right = (CategoryTheory.Bicategory.rightUnitor t.extension).hom
<VAR>B : Type u<VAR>CategoryTheory.Bicategory B<VAR>a b c : B<VAR>f : b ⟶ a<VAR>g : c ⟶ a<VAR>s t : CategoryTheory.Bicategory.LeftLift f g<VAR>h : s ⟶ t<GOAL>CategoryTheory.CategoryStruct.comp s.unit (CategoryTheory.Bicategory.whiskerRight h.right f) = t.unit
<VAR>B : Type u<VAR>CategoryTheory.Bicategory B<VAR>a b c : B<VAR>f : b ⟶ a<VAR>g : c ⟶ a<VAR>t : CategoryTheory.Bicategory.LeftLift f (CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id c) g)<GOAL>t.ofIdComp.right = t.lift
<VAR>B : Type u<VAR>CategoryTheory.Bicategory B<VAR>a b c : B<VAR>f : b ⟶ a<VAR>g : c ⟶ a<VAR>t : CategoryTheory.Bicategory.LeftLift f (CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id c) g)<GOAL>t.ofIdComp.hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.leftUnitor g).inv t.unit
<VAR>B : Type u<VAR>CategoryTheory.Bicategory B<VAR>a b c : B<VAR>f : b ⟶ a<VAR>g : c ⟶ a<VAR>t : CategoryTheory.Bicategory.LeftLift f (CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id c) g)<GOAL>t.ofIdComp.left.as = PUnit.unit
<VAR>B : Type u<VAR>CategoryTheory.Bicategory B<VAR>a b c : B<VAR>f : b ⟶ a<VAR>g : c ⟶ a<VAR>t : CategoryTheory.Bicategory.LeftLift f g<VAR>x : B<VAR>h : x ⟶ c<GOAL>(t.whisker h).lift = CategoryTheory.CategoryStruct.comp h t.lift
<VAR>B : Type u<VAR>CategoryTheory.Bicategory B<VAR>a b c : B<VAR>f : b ⟶ a<VAR>g : c ⟶ a<VAR>t : CategoryTheory.Bicategory.LeftLift f g<VAR>x : B<VAR>h : x ⟶ c<GOAL>(t.whisker h).unit = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft h t.unit) (CategoryTheory.Bicategory.associator h t.lift f).inv
<VAR>B : Type u<VAR>CategoryTheory.Bicategory B<VAR>a b c : B<VAR>f : b ⟶ a<VAR>g : c ⟶ a<VAR>x : B<VAR>h : x ⟶ c<GOAL>∀ {X Y : CategoryTheory.Bicategory.LeftLift f g} (η : X ⟶ Y), (CategoryTheory.Bicategory.LeftLift.whiskering h).map η = CategoryTheory.Bicategory.LeftLift.homMk (CategoryTheory.Bicategory.whiskerLeft h η.right) ⋯
<VAR>B : Type u<VAR>CategoryTheory.Bicategory B<VAR>a b c : B<VAR>f : b ⟶ a<VAR>g : c ⟶ a<VAR>x : B<VAR>h : x ⟶ c<VAR>t : CategoryTheory.Bicategory.LeftLift f g<GOAL>(CategoryTheory.Bicategory.LeftLift.whiskering h).obj t = t.whisker h
<VAR>B : Type u<VAR>CategoryTheory.Bicategory B<VAR>a b c : B<VAR>f : b ⟶ a<VAR>g : c ⟶ a<VAR>s : CategoryTheory.Bicategory.LeftLift f (CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id c) g)<VAR>t : CategoryTheory.Bicategory.LeftLift f g<VAR>τ : s ⟶ t.whisker (CategoryTheory.CategoryStruct.id c)<GOAL>(s.whiskerIdCancel τ).right = CategoryTheory.CategoryStruct.comp τ.right (CategoryTheory.Bicategory.leftUnitor t.lift).hom
<VAR>B : Type u<VAR>CategoryTheory.Bicategory B<VAR>a b c : B<VAR>f : b ⟶ a<VAR>g : c ⟶ a<VAR>s t : CategoryTheory.Bicategory.LeftLift f g<VAR>i : s ⟶ t<VAR>x : B<VAR>h : x ⟶ c<GOAL>(CategoryTheory.Bicategory.LeftLift.whiskerHom i h).right = CategoryTheory.Bicategory.whiskerLeft h i.right
<VAR>B : Type u<VAR>CategoryTheory.Bicategory B<VAR>a b c : B<VAR>f : b ⟶ a<VAR>g : c ⟶ a<VAR>t : CategoryTheory.Bicategory.LeftLift f g<GOAL>t.whiskerOfIdCompIsoSelf.hom.right = (CategoryTheory.Bicategory.leftUnitor t.lift).hom
<VAR>B : Type u<VAR>CategoryTheory.Bicategory B<VAR>a b c : B<VAR>f : b ⟶ a<VAR>g : c ⟶ a<VAR>t : CategoryTheory.Bicategory.LeftLift f g<GOAL>t.whiskerOfIdCompIsoSelf.inv.right = (CategoryTheory.Bicategory.leftUnitor t.lift).inv
<VAR>B : Type u<VAR>CategoryTheory.Bicategory B<VAR>a b c : B<VAR>f : a ⟶ b<VAR>g : a ⟶ c<VAR>s t : CategoryTheory.Bicategory.RightExtension f g<VAR>η : s ⟶ t<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft f η.left) t.counit = s.counit
<VAR>B : Type u<VAR>CategoryTheory.Bicategory B<VAR>a b c : B<VAR>f : b ⟶ a<VAR>g : c ⟶ a<VAR>s t : CategoryTheory.Bicategory.RightLift f g<VAR>h : s ⟶ t<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight h.left f) t.counit = s.counit
<VAR>B : Type u₁<VAR>CategoryTheory.Bicategory B<VAR>C : Type u₂<VAR>CategoryTheory.Bicategory C<VAR>self : CategoryTheory.LaxFunctor B C<VAR>a b : B<VAR>f : a ⟶ b<GOAL>self.map₂ (CategoryTheory.Bicategory.rightUnitor f).inv = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.rightUnitor (self.map f)).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (self.map f) (self.mapId b)) (self.mapComp f (CategoryTheory.CategoryStruct.id b)))
<VAR>B : Type u₁<VAR>CategoryTheory.Bicategory B<VAR>C : Type u₂<VAR>CategoryTheory.Bicategory C<VAR>self : CategoryTheory.LaxFunctor B C<VAR>a b c : B<VAR>f f' : a ⟶ b<VAR>η : f ⟶ f'<VAR>g : b ⟶ c<GOAL>CategoryTheory.CategoryStruct.comp (self.mapComp f g) (self.map₂ (CategoryTheory.Bicategory.whiskerRight η g)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (self.map₂ η) (self.map g)) (self.mapComp f' g)
<VAR>B : Type u₁<VAR>CategoryTheory.Bicategory B<VAR>C : Type u₂<VAR>CategoryTheory.Bicategory C<VAR>self : CategoryTheory.LaxFunctor B C<VAR>a b c d : B<VAR>f : a ⟶ b<VAR>g : b ⟶ c<VAR>h : c ⟶ d<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (self.mapComp f g) (self.map h)) (CategoryTheory.CategoryStruct.comp (self.mapComp (CategoryTheory.CategoryStruct.comp f g) h) (self.map₂ (CategoryTheory.Bicategory.associator f g h).hom)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (self.map f) (self.map g) (self.map h)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (self.map f) (self.mapComp g h)) (self.mapComp f (CategoryTheory.CategoryStruct.comp g h)))
<VAR>B : Type u₁<VAR>CategoryTheory.Bicategory B<VAR>C : Type u₂<VAR>CategoryTheory.Bicategory C<VAR>self : CategoryTheory.LaxFunctor B C<VAR>a b : B<VAR>f : a ⟶ b<GOAL>self.map₂ (CategoryTheory.Bicategory.leftUnitor f).inv = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.leftUnitor (self.map f)).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (self.mapId a) (self.map f)) (self.mapComp (CategoryTheory.CategoryStruct.id a) f))
<VAR>B : Type u₁<VAR>CategoryTheory.Bicategory B<VAR>C : Type u₂<VAR>CategoryTheory.Bicategory C<VAR>self : CategoryTheory.LaxFunctor B C<VAR>a b c : B<VAR>f : a ⟶ b<VAR>g g' : b ⟶ c<VAR>η : g ⟶ g'<GOAL>CategoryTheory.CategoryStruct.comp (self.mapComp f g) (self.map₂ (CategoryTheory.Bicategory.whiskerLeft f η)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (self.map f) (self.map₂ η)) (self.mapComp f g')
<VAR>B : Type u₁<VAR>CategoryTheory.Bicategory B<VAR>C : Type u₂<VAR>CategoryTheory.Bicategory C<VAR>F : CategoryTheory.LaxFunctor B C<VAR>a b c d : B<VAR>f : a ⟶ b<VAR>g : b ⟶ c<VAR>h : c ⟶ d<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (F.mapComp f g) (F.map h)) (F.mapComp (CategoryTheory.CategoryStruct.comp f g) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (F.map f) (F.map g) (F.map h)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (F.map f) (F.mapComp g h)) (CategoryTheory.CategoryStruct.comp (F.mapComp f (CategoryTheory.CategoryStruct.comp g h)) (F.map₂ (CategoryTheory.Bicategory.associator f g h).inv)))
<VAR>B : Type u₁<VAR>CategoryTheory.Bicategory B<VAR>C : Type u₂<VAR>CategoryTheory.Bicategory C<VAR>F : CategoryTheory.LaxFunctor B C<VAR>a b c d : B<VAR>f : a ⟶ b<VAR>g : b ⟶ c<VAR>h : c ⟶ d<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (F.map f) (F.mapComp g h)) (F.mapComp f (CategoryTheory.CategoryStruct.comp g h)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (F.map f) (F.map g) (F.map h)).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (F.mapComp f g) (F.map h)) (CategoryTheory.CategoryStruct.comp (F.mapComp (CategoryTheory.CategoryStruct.comp f g) h) (F.map₂ (CategoryTheory.Bicategory.associator f g h).hom)))
<VAR>B : Type u₁<VAR>CategoryTheory.Bicategory B<VAR>C : Type u₂<VAR>CategoryTheory.Bicategory C<VAR>F : CategoryTheory.LaxFunctor B C<VAR>a b : B<VAR>f : a ⟶ b<GOAL>(CategoryTheory.Bicategory.leftUnitor (F.map f)).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (F.mapId a) (F.map f)) (CategoryTheory.CategoryStruct.comp (F.mapComp (CategoryTheory.CategoryStruct.id a) f) (F.map₂ (CategoryTheory.Bicategory.leftUnitor f).hom))
<VAR>B : Type u₁<VAR>CategoryTheory.Bicategory B<VAR>C : Type u₂<VAR>CategoryTheory.Bicategory C<VAR>F : CategoryTheory.LaxFunctor B C<VAR>a b : B<VAR>f : a ⟶ b<GOAL>(CategoryTheory.Bicategory.rightUnitor (F.map f)).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (F.map f) (F.mapId b)) (CategoryTheory.CategoryStruct.comp (F.mapComp f (CategoryTheory.CategoryStruct.id b)) (F.map₂ (CategoryTheory.Bicategory.rightUnitor f).hom))
<VAR>B : Type u₁<VAR>CategoryTheory.Bicategory B<GOAL>(CategoryTheory.LaxFunctor.id B).toPrelaxFunctor = CategoryTheory.PrelaxFunctor.id B
<VAR>B : Type u₁<VAR>CategoryTheory.Bicategory B<GOAL>∀ {a b c : B} (f : a ⟶ b) (g : b ⟶ c), (CategoryTheory.LaxFunctor.id B).mapComp f g = CategoryTheory.CategoryStruct.id (CategoryTheory.CategoryStruct.comp f g)
<VAR>B : Type u₁<VAR>CategoryTheory.Bicategory B<VAR>a : B<GOAL>(CategoryTheory.LaxFunctor.id B).mapId a = CategoryTheory.CategoryStruct.id (CategoryTheory.CategoryStruct.id a)
<VAR>B : Type u₁<VAR>CategoryTheory.Bicategory B<VAR>C : Type u₂<VAR>CategoryTheory.Bicategory C<VAR>D : Type u₃<VAR>CategoryTheory.Bicategory D<VAR>F : CategoryTheory.LaxFunctor B C<VAR>G : CategoryTheory.LaxFunctor C D<GOAL>(F.comp G).toPrelaxFunctor = F.comp G.toPrelaxFunctor
<VAR>B : Type u₁<VAR>CategoryTheory.Bicategory B<VAR>C : Type u₂<VAR>CategoryTheory.Bicategory C<VAR>D : Type u₃<VAR>CategoryTheory.Bicategory D<VAR>F : CategoryTheory.LaxFunctor B C<VAR>G : CategoryTheory.LaxFunctor C D<VAR>a : B<GOAL>(F.comp G).mapId a = CategoryTheory.CategoryStruct.comp (G.mapId (F.obj a)) (G.map₂ (F.mapId a))
<VAR>B : Type u₁<VAR>CategoryTheory.Bicategory B<VAR>C : Type u₂<VAR>CategoryTheory.Bicategory C<VAR>D : Type u₃<VAR>CategoryTheory.Bicategory D<VAR>F : CategoryTheory.LaxFunctor B C<VAR>G : CategoryTheory.LaxFunctor C D<GOAL>∀ {a b c : B} (f : a ⟶ b) (g : b ⟶ c), (F.comp G).mapComp f g = CategoryTheory.CategoryStruct.comp (G.mapComp (F.map f) (F.map g)) (G.map₂ (F.mapComp f g))
<VAR>B : Type u₁<VAR>CategoryTheory.Bicategory B<VAR>C : Type u₂<VAR>CategoryTheory.Bicategory C<VAR>F : CategoryTheory.LaxFunctor B C<VAR>self : F.PseudoCore<VAR>a b c : B<VAR>f : a ⟶ b<VAR>g : b ⟶ c<GOAL>(self.mapCompIso f g).inv = F.mapComp f g
<VAR>B : Type u₁<VAR>CategoryTheory.Bicategory B<VAR>C : Type u₂<VAR>CategoryTheory.Bicategory C<VAR>F : CategoryTheory.LaxFunctor B C<VAR>self : F.PseudoCore<VAR>a : B<GOAL>(self.mapIdIso a).inv = F.mapId a
<VAR>B : Type u₁<VAR>CategoryTheory.Bicategory B<VAR>C : Type u₂<VAR>CategoryTheory.Bicategory C<VAR>self : CategoryTheory.OplaxFunctor B C<VAR>a b c : B<VAR>f f' : a ⟶ b<VAR>η : f ⟶ f'<VAR>g : b ⟶ c<GOAL>CategoryTheory.CategoryStruct.comp (self.map₂ (CategoryTheory.Bicategory.whiskerRight η g)) (self.mapComp f' g) = CategoryTheory.CategoryStruct.comp (self.mapComp f g) (CategoryTheory.Bicategory.whiskerRight (self.map₂ η) (self.map g))
<VAR>B : Type u₁<VAR>CategoryTheory.Bicategory B<VAR>C : Type u₂<VAR>CategoryTheory.Bicategory C<VAR>self : CategoryTheory.OplaxFunctor B C<VAR>a b : B<VAR>f : a ⟶ b<GOAL>self.map₂ (CategoryTheory.Bicategory.leftUnitor f).hom = CategoryTheory.CategoryStruct.comp (self.mapComp (CategoryTheory.CategoryStruct.id a) f) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (self.mapId a) (self.map f)) (CategoryTheory.Bicategory.leftUnitor (self.map f)).hom)
<VAR>B : Type u₁<VAR>CategoryTheory.Bicategory B<VAR>C : Type u₂<VAR>CategoryTheory.Bicategory C<VAR>self : CategoryTheory.OplaxFunctor B C<VAR>a b c d : B<VAR>f : a ⟶ b<VAR>g : b ⟶ c<VAR>h : c ⟶ d<GOAL>CategoryTheory.CategoryStruct.comp (self.map₂ (CategoryTheory.Bicategory.associator f g h).hom) (CategoryTheory.CategoryStruct.comp (self.mapComp f (CategoryTheory.CategoryStruct.comp g h)) (CategoryTheory.Bicategory.whiskerLeft (self.map f) (self.mapComp g h))) = CategoryTheory.CategoryStruct.comp (self.mapComp (CategoryTheory.CategoryStruct.comp f g) h) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (self.mapComp f g) (self.map h)) (CategoryTheory.Bicategory.associator (self.map f) (self.map g) (self.map h)).hom)
<VAR>B : Type u₁<VAR>CategoryTheory.Bicategory B<VAR>C : Type u₂<VAR>CategoryTheory.Bicategory C<VAR>self : CategoryTheory.OplaxFunctor B C<VAR>a b c : B<VAR>f : a ⟶ b<VAR>g g' : b ⟶ c<VAR>η : g ⟶ g'<GOAL>CategoryTheory.CategoryStruct.comp (self.map₂ (CategoryTheory.Bicategory.whiskerLeft f η)) (self.mapComp f g') = CategoryTheory.CategoryStruct.comp (self.mapComp f g) (CategoryTheory.Bicategory.whiskerLeft (self.map f) (self.map₂ η))
<VAR>B : Type u₁<VAR>CategoryTheory.Bicategory B<VAR>C : Type u₂<VAR>CategoryTheory.Bicategory C<VAR>self : CategoryTheory.OplaxFunctor B C<VAR>a b : B<VAR>f : a ⟶ b<GOAL>self.map₂ (CategoryTheory.Bicategory.rightUnitor f).hom = CategoryTheory.CategoryStruct.comp (self.mapComp f (CategoryTheory.CategoryStruct.id b)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (self.map f) (self.mapId b)) (CategoryTheory.Bicategory.rightUnitor (self.map f)).hom)
<VAR>B : Type u₁<VAR>CategoryTheory.Bicategory B<VAR>C : Type u₂<VAR>CategoryTheory.Bicategory C<VAR>F : CategoryTheory.OplaxFunctor B C<VAR>a b c d : B<VAR>f : a ⟶ b<VAR>g : b ⟶ c<VAR>h : c ⟶ d<GOAL>CategoryTheory.CategoryStruct.comp (F.mapComp f (CategoryTheory.CategoryStruct.comp g h)) (CategoryTheory.Bicategory.whiskerLeft (F.map f) (F.mapComp g h)) = CategoryTheory.CategoryStruct.comp (F.map₂ (CategoryTheory.Bicategory.associator f g h).inv) (CategoryTheory.CategoryStruct.comp (F.mapComp (CategoryTheory.CategoryStruct.comp f g) h) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (F.mapComp f g) (F.map h)) (CategoryTheory.Bicategory.associator (F.map f) (F.map g) (F.map h)).hom))
<VAR>B : Type u₁<VAR>CategoryTheory.Bicategory B<VAR>C : Type u₂<VAR>CategoryTheory.Bicategory C<VAR>F : CategoryTheory.OplaxFunctor B C<VAR>a b c d : B<VAR>f : a ⟶ b<VAR>g : b ⟶ c<VAR>h : c ⟶ d<GOAL>CategoryTheory.CategoryStruct.comp (F.mapComp (CategoryTheory.CategoryStruct.comp f g) h) (CategoryTheory.Bicategory.whiskerRight (F.mapComp f g) (F.map h)) = CategoryTheory.CategoryStruct.comp (F.map₂ (CategoryTheory.Bicategory.associator f g h).hom) (CategoryTheory.CategoryStruct.comp (F.mapComp f (CategoryTheory.CategoryStruct.comp g h)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (F.map f) (F.mapComp g h)) (CategoryTheory.Bicategory.associator (F.map f) (F.map g) (F.map h)).inv))
<VAR>B : Type u₁<VAR>CategoryTheory.Bicategory B<VAR>a : B<GOAL>(CategoryTheory.OplaxFunctor.id B).mapId a = CategoryTheory.CategoryStruct.id (CategoryTheory.CategoryStruct.id a)
<VAR>B : Type u₁<VAR>CategoryTheory.Bicategory B<GOAL>∀ {a b c : B} (f : a ⟶ b) (g : b ⟶ c), (CategoryTheory.OplaxFunctor.id B).mapComp f g = CategoryTheory.CategoryStruct.id (CategoryTheory.CategoryStruct.comp f g)
<VAR>B : Type u₁<VAR>CategoryTheory.Bicategory B<GOAL>(CategoryTheory.OplaxFunctor.id B).toPrelaxFunctor = CategoryTheory.PrelaxFunctor.id B
<VAR>B : Type u₁<VAR>CategoryTheory.Bicategory B<VAR>C : Type u₂<VAR>CategoryTheory.Bicategory C<VAR>F : CategoryTheory.OplaxFunctor B C<VAR>self : F.PseudoCore<VAR>a b c : B<VAR>f : a ⟶ b<VAR>g : b ⟶ c<GOAL>(self.mapCompIso f g).hom = F.mapComp f g
<VAR>B : Type u₁<VAR>CategoryTheory.Bicategory B<VAR>C : Type u₂<VAR>CategoryTheory.Bicategory C<VAR>F : CategoryTheory.OplaxFunctor B C<VAR>self : F.PseudoCore<VAR>a : B<GOAL>(self.mapIdIso a).hom = F.mapId a
<VAR>c : Type u → Type u<VAR>hom : ⦃α β : Type u⦄ → c α → c β → Type u<VAR>self : CategoryTheory.BundledHom hom<VAR>α β γ : Type u<VAR>Iα : c α<VAR>Iβ : c β<VAR>Iγ : c γ<VAR>f : hom Iα Iβ<VAR>g : hom Iβ Iγ<GOAL>self.toFun Iα Iγ (self.comp Iα Iβ Iγ g f) = self.toFun Iβ Iγ g ∘ self.toFun Iα Iβ f
<VAR>c : Type u → Type u<VAR>hom : ⦃α β : Type u⦄ → c α → c β → Type u<VAR>self : CategoryTheory.BundledHom hom<VAR>α : Type u<VAR>I : c α<GOAL>self.toFun I I (self.id I) = id
<VAR>c : Type u → Type u<VAR>hom : ⦃α β : Type u⦄ → c α → c β → Type u<VAR>self : CategoryTheory.BundledHom hom<VAR>α β : Type u<VAR>Iα : c α<VAR>Iβ : c β<GOAL>Function.Injective (self.toFun Iα Iβ)