case mk
C : Type u₁
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
toPrefunctor✝ : Cᵒᵖ ⥤q D
map_id✝ : ∀ (X : Cᵒᵖ), toPrefunctor✝.map (𝟙 X) = 𝟙 (toPrefunctor✝.obj X)
map_comp✝ :
  ∀ {X Y Z : Cᵒᵖ} (f : X ⟶ Y) (g : Y ⟶ Z), toPrefunctor✝.map (f ≫ g) = toPrefunctor✝.map f ≫ toPrefunctor✝.map g
⊢ (mk toPrefunctor✝).rightOp.leftOp = mk toPrefunctor✝
C : Type u₁
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
F : Cᵒᵖ ⥤ D
⊢ F.rightOp.leftOp = F
cases F
no goals
case mk
C : Type u₁
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
toPrefunctor✝ : Cᵒᵖ ⥤q D
map_id✝ : ∀ (X : Cᵒᵖ), toPrefunctor✝.map (𝟙 X) = 𝟙 (toPrefunctor✝.obj X)
map_comp✝ :
  ∀ {X Y Z : Cᵒᵖ} (f : X ⟶ Y) (g : Y ⟶ Z), toPrefunctor✝.map (f ≫ g) = toPrefunctor✝.map f ≫ toPrefunctor✝.map g
⊢ (mk toPrefunctor✝).rightOp.leftOp = mk toPrefunctor✝
rfl