ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>B : Type u<VAR>CategoryTheory.Bicategory B<VAR>a b c : B<VAR>f : a ⟶ b<VAR>g h : b ⟶ c<VAR>η : g ≅ h<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft f η.hom) (CategoryTheory.Bicategory.whiskerLeft f η.inv) = CategoryTheory.CategoryStruct.id (CategoryTheory.CategoryStruct.comp f g)
<VAR>B : Type u<VAR>CategoryTheory.Bicategory B<VAR>a b c : B<VAR>f g : a ⟶ b<VAR>η : f ≅ g<VAR>h : b ⟶ c<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight η.hom h) (CategoryTheory.Bicategory.whiskerRight η.inv h) = CategoryTheory.CategoryStruct.id (CategoryTheory.CategoryStruct.comp f h)
<VAR>B : Type u<VAR>CategoryTheory.Bicategory B<VAR>a b c : B<VAR>f : a ⟶ b<VAR>g h : b ⟶ c<VAR>η : g ≅ h<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft f η.inv) (CategoryTheory.Bicategory.whiskerLeft f η.hom) = CategoryTheory.CategoryStruct.id (CategoryTheory.CategoryStruct.comp f h)
<VAR>B : Type u<VAR>CategoryTheory.Bicategory B<VAR>a b c : B<VAR>f g : a ⟶ b<VAR>η : f ≅ g<VAR>h : b ⟶ c<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight η.inv h) (CategoryTheory.Bicategory.whiskerRight η.hom h) = CategoryTheory.CategoryStruct.id (CategoryTheory.CategoryStruct.comp g h)
<VAR>B : Type u<VAR>CategoryTheory.Bicategory B<VAR>a b c : B<VAR>f : a ⟶ b<VAR>g h : b ⟶ c<VAR>η : g ≅ h<GOAL>(CategoryTheory.Bicategory.whiskerLeftIso f η).inv = CategoryTheory.Bicategory.whiskerLeft f η.inv
<VAR>B : Type u<VAR>CategoryTheory.Bicategory B<VAR>a b c : B<VAR>f : a ⟶ b<VAR>g h : b ⟶ c<VAR>η : g ≅ h<GOAL>(CategoryTheory.Bicategory.whiskerLeftIso f η).hom = CategoryTheory.Bicategory.whiskerLeft f η.hom
<VAR>B : Type u<VAR>CategoryTheory.Bicategory B<VAR>a b c : B<VAR>f : a ⟶ b<VAR>g h : b ⟶ c<VAR>η : g ⟶ h<VAR>CategoryTheory.IsIso η<GOAL>CategoryTheory.inv (CategoryTheory.Bicategory.whiskerLeft f η) = CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.inv η)
<VAR>B : Type u<VAR>CategoryTheory.Bicategory B<VAR>a b c : B<VAR>f g : a ⟶ b<VAR>η : f ≅ g<VAR>h : b ⟶ c<GOAL>(CategoryTheory.Bicategory.whiskerRightIso η h).hom = CategoryTheory.Bicategory.whiskerRight η.hom h
<VAR>B : Type u<VAR>CategoryTheory.Bicategory B<VAR>a b c : B<VAR>f g : a ⟶ b<VAR>η : f ≅ g<VAR>h : b ⟶ c<GOAL>(CategoryTheory.Bicategory.whiskerRightIso η h).inv = CategoryTheory.Bicategory.whiskerRight η.inv h
<VAR>B : Type u<VAR>CategoryTheory.Bicategory B<VAR>a b c : B<VAR>f g : a ⟶ b<VAR>η : f ⟶ g<VAR>h : b ⟶ c<VAR>CategoryTheory.IsIso η<GOAL>CategoryTheory.inv (CategoryTheory.Bicategory.whiskerRight η h) = CategoryTheory.Bicategory.whiskerRight (CategoryTheory.inv η) h
<VAR>B : Type u<VAR>CategoryTheory.Bicategory B<VAR>a b c d e : B<VAR>f : a ⟶ b<VAR>g : b ⟶ c<VAR>h : c ⟶ d<VAR>i : d ⟶ e<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.associator g h i).inv) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator f (CategoryTheory.CategoryStruct.comp g h) i).inv (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.associator f g h).inv i)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator f g (CategoryTheory.CategoryStruct.comp h i)).inv (CategoryTheory.Bicategory.associator (CategoryTheory.CategoryStruct.comp f g) h i).inv
<VAR>B : Type u<VAR>CategoryTheory.Bicategory B<VAR>a b c d e : B<VAR>f : a ⟶ b<VAR>g : b ⟶ c<VAR>h : c ⟶ d<VAR>i : d ⟶ e<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator f (CategoryTheory.CategoryStruct.comp g h) i).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.associator f g h).inv i) (CategoryTheory.Bicategory.associator (CategoryTheory.CategoryStruct.comp f g) h i).hom) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.associator g h i).hom) (CategoryTheory.Bicategory.associator f g (CategoryTheory.CategoryStruct.comp h i)).inv
<VAR>B : Type u<VAR>CategoryTheory.Bicategory B<VAR>a b c d e : B<VAR>f : a ⟶ b<VAR>g : b ⟶ c<VAR>h : c ⟶ d<VAR>i : d ⟶ e<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (CategoryTheory.CategoryStruct.comp f g) h i).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.associator f g h).hom i) (CategoryTheory.Bicategory.associator f (CategoryTheory.CategoryStruct.comp g h) i).hom) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator f g (CategoryTheory.CategoryStruct.comp h i)).hom (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.associator g h i).inv)
<VAR>B : Type u<VAR>CategoryTheory.Bicategory B<VAR>a b c d e : B<VAR>f : a ⟶ b<VAR>g : b ⟶ c<VAR>h : c ⟶ d<VAR>i : d ⟶ e<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.associator g h i).hom) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator f g (CategoryTheory.CategoryStruct.comp h i)).inv (CategoryTheory.Bicategory.associator (CategoryTheory.CategoryStruct.comp f g) h i).inv) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator f (CategoryTheory.CategoryStruct.comp g h) i).inv (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.associator f g h).inv i)
<VAR>B : Type u<VAR>CategoryTheory.Bicategory B<VAR>a b c d e : B<VAR>f : a ⟶ b<VAR>g : b ⟶ c<VAR>h : c ⟶ d<VAR>i : d ⟶ e<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (CategoryTheory.CategoryStruct.comp f g) h i).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator f g (CategoryTheory.CategoryStruct.comp h i)).hom (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.associator g h i).inv)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.associator f g h).hom i) (CategoryTheory.Bicategory.associator f (CategoryTheory.CategoryStruct.comp g h) i).hom
<VAR>B : Type u<VAR>CategoryTheory.Bicategory B<VAR>a b c d e : B<VAR>f : a ⟶ b<VAR>g : b ⟶ c<VAR>h : c ⟶ d<VAR>i : d ⟶ e<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator f g (CategoryTheory.CategoryStruct.comp h i)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.associator g h i).inv) (CategoryTheory.Bicategory.associator f (CategoryTheory.CategoryStruct.comp g h) i).inv) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (CategoryTheory.CategoryStruct.comp f g) h i).inv (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.associator f g h).hom i)
<VAR>B : Type u<VAR>CategoryTheory.Bicategory B<VAR>a b c d e : B<VAR>f : a ⟶ b<VAR>g : b ⟶ c<VAR>h : c ⟶ d<VAR>i : d ⟶ e<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator f (CategoryTheory.CategoryStruct.comp g h) i).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.associator g h i).hom) (CategoryTheory.Bicategory.associator f g (CategoryTheory.CategoryStruct.comp h i)).inv) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.associator f g h).inv i) (CategoryTheory.Bicategory.associator (CategoryTheory.CategoryStruct.comp f g) h i).hom
<VAR>B : Type u<VAR>CategoryTheory.Bicategory B<VAR>a b c d e : B<VAR>f : a ⟶ b<VAR>g : b ⟶ c<VAR>h : c ⟶ d<VAR>i : d ⟶ e<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.associator f g h).inv i) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (CategoryTheory.CategoryStruct.comp f g) h i).hom (CategoryTheory.Bicategory.associator f g (CategoryTheory.CategoryStruct.comp h i)).hom) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator f (CategoryTheory.CategoryStruct.comp g h) i).hom (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.associator g h i).hom)
<VAR>B : Type u<VAR>CategoryTheory.Bicategory B<VAR>a b c d e : B<VAR>f : a ⟶ b<VAR>g : b ⟶ c<VAR>h : c ⟶ d<VAR>i : d ⟶ e<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator f g (CategoryTheory.CategoryStruct.comp h i)).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (CategoryTheory.CategoryStruct.comp f g) h i).inv (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.associator f g h).hom i)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.associator g h i).inv) (CategoryTheory.Bicategory.associator f (CategoryTheory.CategoryStruct.comp g h) i).inv
<VAR>B : Type u<VAR>CategoryTheory.Bicategory B<VAR>a b c : B<VAR>f : a ⟶ b<VAR>g : b ⟶ c<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator f (CategoryTheory.CategoryStruct.id b) g).hom (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.leftUnitor g).hom) = CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.rightUnitor f).hom g
<VAR>B : Type u<VAR>CategoryTheory.Bicategory B<VAR>a b c : B<VAR>f : a ⟶ b<VAR>g : b ⟶ c<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator f (CategoryTheory.CategoryStruct.id b) g).inv (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.rightUnitor f).hom g) = CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.leftUnitor g).hom
<VAR>B : Type u<VAR>CategoryTheory.Bicategory B<VAR>a b c : B<VAR>f : a ⟶ b<VAR>g : b ⟶ c<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.rightUnitor f).inv g) (CategoryTheory.Bicategory.associator f (CategoryTheory.CategoryStruct.id b) g).hom = CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.leftUnitor g).inv
<VAR>B : Type u<VAR>CategoryTheory.Bicategory B<VAR>a b c : B<VAR>f : a ⟶ b<VAR>g : b ⟶ c<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.leftUnitor g).inv) (CategoryTheory.Bicategory.associator f (CategoryTheory.CategoryStruct.id b) g).inv = CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.rightUnitor f).inv g
<VAR>B : Type u<VAR>CategoryTheory.Bicategory B<VAR>a b c d : B<VAR>f f' : a ⟶ b<VAR>η : f ⟶ f'<VAR>g : b ⟶ c<VAR>h : c ⟶ d<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.whiskerRight η g) h) (CategoryTheory.Bicategory.associator f' g h).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator f g h).hom (CategoryTheory.Bicategory.whiskerRight η (CategoryTheory.CategoryStruct.comp g h))
<VAR>B : Type u<VAR>CategoryTheory.Bicategory B<VAR>a b c d : B<VAR>f f' : a ⟶ b<VAR>η : f ⟶ f'<VAR>g : b ⟶ c<VAR>h : c ⟶ d<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight η (CategoryTheory.CategoryStruct.comp g h)) (CategoryTheory.Bicategory.associator f' g h).inv = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator f g h).inv (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.whiskerRight η g) h)
<VAR>B : Type u<VAR>CategoryTheory.Bicategory B<VAR>a b c d : B<VAR>f f' : a ⟶ b<VAR>η : f ⟶ f'<VAR>g : b ⟶ c<VAR>h : c ⟶ d<GOAL>CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.whiskerRight η g) h = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator f g h).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight η (CategoryTheory.CategoryStruct.comp g h)) (CategoryTheory.Bicategory.associator f' g h).inv)
<VAR>B : Type u<VAR>CategoryTheory.Bicategory B<VAR>a b c d : B<VAR>f : a ⟶ b<VAR>g g' : b ⟶ c<VAR>η : g ⟶ g'<VAR>h : c ⟶ d<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.whiskerLeft f η) h) (CategoryTheory.Bicategory.associator f g' h).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator f g h).hom (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.whiskerRight η h))
<VAR>B : Type u<VAR>CategoryTheory.Bicategory B<VAR>a b c d : B<VAR>f : a ⟶ b<VAR>g g' : b ⟶ c<VAR>η : g ⟶ g'<VAR>h : c ⟶ d<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.whiskerRight η h)) (CategoryTheory.Bicategory.associator f g' h).inv = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator f g h).inv (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.whiskerLeft f η) h)
<VAR>B : Type u<VAR>CategoryTheory.Bicategory B<VAR>a b c d : B<VAR>f : a ⟶ b<VAR>g g' : b ⟶ c<VAR>η : g ⟶ g'<VAR>h : c ⟶ d<GOAL>CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.whiskerRight η h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator f g h).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.whiskerLeft f η) h) (CategoryTheory.Bicategory.associator f g' h).hom)
<VAR>B : Type u<VAR>CategoryTheory.Bicategory B<VAR>a b c d : B<VAR>f : a ⟶ b<VAR>g : b ⟶ c<VAR>h h' : c ⟶ d<VAR>η : h ⟶ h'<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (CategoryTheory.CategoryStruct.comp f g) η) (CategoryTheory.Bicategory.associator f g h').hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator f g h).hom (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.whiskerLeft g η))
<VAR>B : Type u<VAR>CategoryTheory.Bicategory B<VAR>a b c d : B<VAR>f : a ⟶ b<VAR>g : b ⟶ c<VAR>h h' : c ⟶ d<VAR>η : h ⟶ h'<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.whiskerLeft g η)) (CategoryTheory.Bicategory.associator f g h').inv = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator f g h).inv (CategoryTheory.Bicategory.whiskerLeft (CategoryTheory.CategoryStruct.comp f g) η)
<VAR>B : Type u<VAR>CategoryTheory.Bicategory B<VAR>a b c d : B<VAR>f : a ⟶ b<VAR>g : b ⟶ c<VAR>h h' : c ⟶ d<VAR>η : h ⟶ h'<GOAL>CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.whiskerLeft g η) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator f g h).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (CategoryTheory.CategoryStruct.comp f g) η) (CategoryTheory.Bicategory.associator f g h').hom)
<VAR>B : Type u<VAR>CategoryTheory.Bicategory B<VAR>a b : B<VAR>f g : a ⟶ b<VAR>η : f ⟶ g<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (CategoryTheory.CategoryStruct.id a) η) (CategoryTheory.Bicategory.leftUnitor g).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.leftUnitor f).hom η
<VAR>B : Type u<VAR>CategoryTheory.Bicategory B<VAR>a b : B<VAR>f g : a ⟶ b<VAR>η : f ⟶ g<GOAL>CategoryTheory.CategoryStruct.comp η (CategoryTheory.Bicategory.leftUnitor g).inv = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.leftUnitor f).inv (CategoryTheory.Bicategory.whiskerLeft (CategoryTheory.CategoryStruct.id a) η)
<VAR>B : Type u<VAR>CategoryTheory.Bicategory B<VAR>a b : B<VAR>f g : a ⟶ b<VAR>η : f ⟶ g<GOAL>η = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.leftUnitor f).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (CategoryTheory.CategoryStruct.id a) η) (CategoryTheory.Bicategory.leftUnitor g).hom)
<VAR>B : Type u<VAR>CategoryTheory.Bicategory B<VAR>a b : B<VAR>f g : a ⟶ b<VAR>η : f ⟶ g<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight η (CategoryTheory.CategoryStruct.id b)) (CategoryTheory.Bicategory.rightUnitor g).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.rightUnitor f).hom η
<VAR>B : Type u<VAR>CategoryTheory.Bicategory B<VAR>a b : B<VAR>f g : a ⟶ b<VAR>η : f ⟶ g<GOAL>CategoryTheory.CategoryStruct.comp η (CategoryTheory.Bicategory.rightUnitor g).inv = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.rightUnitor f).inv (CategoryTheory.Bicategory.whiskerRight η (CategoryTheory.CategoryStruct.id b))
<VAR>B : Type u<VAR>CategoryTheory.Bicategory B<VAR>a b : B<VAR>f g : a ⟶ b<VAR>η : f ⟶ g<GOAL>η = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.rightUnitor f).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight η (CategoryTheory.CategoryStruct.id b)) (CategoryTheory.Bicategory.rightUnitor g).hom)
<VAR>B : Type u<VAR>CategoryTheory.Bicategory B<VAR>a b : B<VAR>f g : a ⟶ b<VAR>η θ : f ⟶ g<GOAL>CategoryTheory.Bicategory.whiskerLeft (CategoryTheory.CategoryStruct.id a) η = CategoryTheory.Bicategory.whiskerLeft (CategoryTheory.CategoryStruct.id a) θ ↔ η = θ
<VAR>B : Type u<VAR>CategoryTheory.Bicategory B<VAR>a b : B<VAR>f g : a ⟶ b<VAR>η θ : f ⟶ g<GOAL>CategoryTheory.Bicategory.whiskerRight η (CategoryTheory.CategoryStruct.id b) = CategoryTheory.Bicategory.whiskerRight θ (CategoryTheory.CategoryStruct.id b) ↔ η = θ
<VAR>B : Type u<VAR>CategoryTheory.Bicategory B<VAR>a b c : B<VAR>f : a ⟶ b<VAR>g : b ⟶ c<GOAL>CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.leftUnitor f).hom g = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (CategoryTheory.CategoryStruct.id a) f g).hom (CategoryTheory.Bicategory.leftUnitor (CategoryTheory.CategoryStruct.comp f g)).hom
<VAR>B : Type u<VAR>CategoryTheory.Bicategory B<VAR>a b c : B<VAR>f : a ⟶ b<VAR>g : b ⟶ c<GOAL>CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.leftUnitor f).inv g = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.leftUnitor (CategoryTheory.CategoryStruct.comp f g)).inv (CategoryTheory.Bicategory.associator (CategoryTheory.CategoryStruct.id a) f g).inv
<VAR>B : Type u<VAR>CategoryTheory.Bicategory B<VAR>a b c : B<VAR>f : a ⟶ b<VAR>g : b ⟶ c<GOAL>CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.rightUnitor g).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator f g (CategoryTheory.CategoryStruct.id c)).inv (CategoryTheory.Bicategory.rightUnitor (CategoryTheory.CategoryStruct.comp f g)).hom
<VAR>B : Type u<VAR>CategoryTheory.Bicategory B<VAR>a b c : B<VAR>f : a ⟶ b<VAR>g : b ⟶ c<GOAL>CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.rightUnitor g).inv = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.rightUnitor (CategoryTheory.CategoryStruct.comp f g)).inv (CategoryTheory.Bicategory.associator f g (CategoryTheory.CategoryStruct.id c)).hom
<VAR>B : Type u<VAR>CategoryTheory.Bicategory B<VAR>a b c : B<VAR>f : a ⟶ b<VAR>g : b ⟶ c<GOAL>(CategoryTheory.Bicategory.leftUnitor (CategoryTheory.CategoryStruct.comp f g)).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (CategoryTheory.CategoryStruct.id a) f g).inv (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.leftUnitor f).hom g)
<VAR>B : Type u<VAR>CategoryTheory.Bicategory B<VAR>a b c : B<VAR>f : a ⟶ b<VAR>g : b ⟶ c<GOAL>(CategoryTheory.Bicategory.leftUnitor (CategoryTheory.CategoryStruct.comp f g)).inv = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.leftUnitor f).inv g) (CategoryTheory.Bicategory.associator (CategoryTheory.CategoryStruct.id a) f g).hom
<VAR>B : Type u<VAR>CategoryTheory.Bicategory B<VAR>a b c : B<VAR>f : a ⟶ b<VAR>g : b ⟶ c<GOAL>(CategoryTheory.Bicategory.rightUnitor (CategoryTheory.CategoryStruct.comp f g)).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator f g (CategoryTheory.CategoryStruct.id c)).hom (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.rightUnitor g).hom)
<VAR>B : Type u<VAR>CategoryTheory.Bicategory B<VAR>a b c : B<VAR>f : a ⟶ b<VAR>g : b ⟶ c<GOAL>(CategoryTheory.Bicategory.rightUnitor (CategoryTheory.CategoryStruct.comp f g)).inv = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.rightUnitor g).inv) (CategoryTheory.Bicategory.associator f g (CategoryTheory.CategoryStruct.id c)).inv
<VAR>B : Type u<VAR>CategoryTheory.Bicategory B<VAR>a : B<GOAL>(CategoryTheory.Bicategory.leftUnitor (CategoryTheory.CategoryStruct.id a)).hom = (CategoryTheory.Bicategory.rightUnitor (CategoryTheory.CategoryStruct.id a)).hom
<VAR>B : Type u<VAR>CategoryTheory.Bicategory B<VAR>a : B<GOAL>(CategoryTheory.Bicategory.leftUnitor (CategoryTheory.CategoryStruct.id a)).inv = (CategoryTheory.Bicategory.rightUnitor (CategoryTheory.CategoryStruct.id a)).inv
<VAR>B : Type u<VAR>CategoryTheory.Bicategory B<VAR>a b : B<VAR>c : B<VAR>f : a ⟶ b<GOAL>∀ (x : b ⟶ c), (CategoryTheory.Bicategory.precomp c f).obj x = CategoryTheory.CategoryStruct.comp f x
<VAR>B : Type u<VAR>CategoryTheory.Bicategory B<VAR>a b : B<VAR>c : B<VAR>f : a ⟶ b<GOAL>∀ {X Y : b ⟶ c} (x : X ⟶ Y), (CategoryTheory.Bicategory.precomp c f).map x = CategoryTheory.Bicategory.whiskerLeft f x
<VAR>B : Type u<VAR>CategoryTheory.Bicategory B<VAR>a b c : B<GOAL>∀ {X Y : a ⟶ b} (η : X ⟶ Y) (x : b ⟶ c), ((CategoryTheory.Bicategory.precomposing a b c).map η).app x = CategoryTheory.Bicategory.whiskerRight η x
<VAR>B : Type u<VAR>CategoryTheory.Bicategory B<VAR>a b c : B<VAR>f : a ⟶ b<GOAL>(CategoryTheory.Bicategory.precomposing a b c).obj f = CategoryTheory.Bicategory.precomp c f
<VAR>B : Type u<VAR>CategoryTheory.Bicategory B<VAR>b c : B<VAR>a : B<VAR>f : b ⟶ c<GOAL>∀ (x : a ⟶ b), (CategoryTheory.Bicategory.postcomp a f).obj x = CategoryTheory.CategoryStruct.comp x f
<VAR>B : Type u<VAR>CategoryTheory.Bicategory B<VAR>b c : B<VAR>a : B<VAR>f : b ⟶ c<GOAL>∀ {X Y : a ⟶ b} (x : X ⟶ Y), (CategoryTheory.Bicategory.postcomp a f).map x = CategoryTheory.Bicategory.whiskerRight x f
<VAR>B : Type u<VAR>CategoryTheory.Bicategory B<VAR>a b c : B<GOAL>∀ {X Y : b ⟶ c} (η : X ⟶ Y) (x : a ⟶ b), ((CategoryTheory.Bicategory.postcomposing a b c).map η).app x = CategoryTheory.Bicategory.whiskerLeft x η
<VAR>B : Type u<VAR>CategoryTheory.Bicategory B<VAR>a b c : B<VAR>f : b ⟶ c<GOAL>(CategoryTheory.Bicategory.postcomposing a b c).obj f = CategoryTheory.Bicategory.postcomp a f
<VAR>B : Type u<VAR>CategoryTheory.Bicategory B<VAR>b c d : B<VAR>a : B<VAR>g : b ⟶ c<VAR>h : c ⟶ d<VAR>X : a ⟶ b<GOAL>(CategoryTheory.Bicategory.associatorNatIsoLeft a g h).inv.app X = (CategoryTheory.Bicategory.associator X g h).inv
<VAR>B : Type u<VAR>CategoryTheory.Bicategory B<VAR>b c d : B<VAR>a : B<VAR>g : b ⟶ c<VAR>h : c ⟶ d<VAR>X : a ⟶ b<GOAL>(CategoryTheory.Bicategory.associatorNatIsoLeft a g h).hom.app X = (CategoryTheory.Bicategory.associator X g h).hom
<VAR>B : Type u<VAR>CategoryTheory.Bicategory B<VAR>a b c d : B<VAR>f : a ⟶ b<VAR>h : c ⟶ d<VAR>X : b ⟶ c<GOAL>(CategoryTheory.Bicategory.associatorNatIsoMiddle f h).inv.app X = (CategoryTheory.Bicategory.associator f X h).inv
<VAR>B : Type u<VAR>CategoryTheory.Bicategory B<VAR>a b c d : B<VAR>f : a ⟶ b<VAR>h : c ⟶ d<VAR>X : b ⟶ c<GOAL>(CategoryTheory.Bicategory.associatorNatIsoMiddle f h).hom.app X = (CategoryTheory.Bicategory.associator f X h).hom
<VAR>B : Type u<VAR>CategoryTheory.Bicategory B<VAR>a b c : B<VAR>f : a ⟶ b<VAR>g : b ⟶ c<VAR>d : B<VAR>X : c ⟶ d<GOAL>(CategoryTheory.Bicategory.associatorNatIsoRight f g d).hom.app X = (CategoryTheory.Bicategory.associator f g X).hom
<VAR>B : Type u<VAR>CategoryTheory.Bicategory B<VAR>a b c : B<VAR>f : a ⟶ b<VAR>g : b ⟶ c<VAR>d : B<VAR>X : c ⟶ d<GOAL>(CategoryTheory.Bicategory.associatorNatIsoRight f g d).inv.app X = (CategoryTheory.Bicategory.associator f g X).inv
<VAR>B : Type u<VAR>CategoryTheory.Bicategory B<VAR>a b : B<VAR>X : a ⟶ b<GOAL>(CategoryTheory.Bicategory.leftUnitorNatIso a b).hom.app X = (CategoryTheory.Bicategory.leftUnitor X).hom
<VAR>B : Type u<VAR>CategoryTheory.Bicategory B<VAR>a b : B<VAR>X : a ⟶ b<GOAL>(CategoryTheory.Bicategory.leftUnitorNatIso a b).inv.app X = (CategoryTheory.Bicategory.leftUnitor X).inv
<VAR>B : Type u<VAR>CategoryTheory.Bicategory B<VAR>a b : B<VAR>X : a ⟶ b<GOAL>(CategoryTheory.Bicategory.rightUnitorNatIso a b).hom.app X = (CategoryTheory.Bicategory.rightUnitor X).hom
<VAR>B : Type u<VAR>CategoryTheory.Bicategory B<VAR>a b : B<VAR>X : a ⟶ b<GOAL>(CategoryTheory.Bicategory.rightUnitorNatIso a b).inv.app X = (CategoryTheory.Bicategory.rightUnitor X).inv