case h_obj
C : Type u
inst✝ : Category C
F : C ⥤ Type w
F₁ F₂ : Cᵒᵖ ⥤ Type v
α : F₁ ⟶ F₂
⊢ ∀ (X : (Functor.Elements F₁)ᵒᵖ),
    (Functor.op (map α) ⋙ toCostructuredArrow F₂).obj X = (toCostructuredArrow F₁ ⋙ CostructuredArrow.map α).obj X

case h_map
C : Type u
inst✝ : Category C
F : C ⥤ Type w
F₁ F₂ : Cᵒᵖ ⥤ Type v
α : F₁ ⟶ F₂
⊢ autoParam
    (∀ (X Y : (Functor.Elements F₁)ᵒᵖ) (f : X ⟶ Y),
      (Functor.op (map α) ⋙ toCostructuredArrow F₂).map f =
        eqToHom (_ : ?F.obj X = ?G.obj X) ≫
          (toCostructuredArrow F₁ ⋙ CostructuredArrow.map α).map f ≫
            eqToHom
              (_ :
                (toCostructuredArrow F₁ ⋙ CostructuredArrow.map α).obj Y =
                  (Functor.op (map α) ⋙ toCostructuredArrow F₂).obj Y))
    _auto✝
C : Type u
inst✝ : Category C
F : C ⥤ Type w
F₁ F₂ : Cᵒᵖ ⥤ Type v
α : F₁ ⟶ F₂
⊢ Functor.op (map α) ⋙ toCostructuredArrow F₂ = toCostructuredArrow F₁ ⋙ CostructuredArrow.map α
fapply Functor.ext
case h_obj
C : Type u
inst✝ : Category C
F : C ⥤ Type w
F₁ F₂ : Cᵒᵖ ⥤ Type v
α : F₁ ⟶ F₂
X : (Functor.Elements F₁)ᵒᵖ
⊢ (Functor.op (map α) ⋙ toCostructuredArrow F₂).obj X = (toCostructuredArrow F₁ ⋙ CostructuredArrow.map α).obj X
case h_obj
C : Type u
inst✝ : Category C
F : C ⥤ Type w
F₁ F₂ : Cᵒᵖ ⥤ Type v
α : F₁ ⟶ F₂
⊢ ∀ (X : (Functor.Elements F₁)ᵒᵖ),
    (Functor.op (map α) ⋙ toCostructuredArrow F₂).obj X = (toCostructuredArrow F₁ ⋙ CostructuredArrow.map α).obj X
intro X
case h_obj
C : Type u
inst✝ : Category C
F : C ⥤ Type w
F₁ F₂ : Cᵒᵖ ⥤ Type v
α : F₁ ⟶ F₂
X : (Functor.Elements F₁)ᵒᵖ
⊢ CostructuredArrow.mk
      ((yonedaSections ((map α).obj X.unop).op.unop.fst.unop F₂).inv { down := ((map α).obj X.unop).op.unop.snd }) =
    CostructuredArrow.mk ((yonedaSections X.unop.fst.unop F₁).inv { down := X.unop.snd } ≫ α)
case h_obj
C : Type u
inst✝ : Category C
F : C ⥤ Type w
F₁ F₂ : Cᵒᵖ ⥤ Type v
α : F₁ ⟶ F₂
X : (Functor.Elements F₁)ᵒᵖ
⊢ (Functor.op (map α) ⋙ toCostructuredArrow F₂).obj X = (toCostructuredArrow F₁ ⋙ CostructuredArrow.map α).obj X
simp only [CostructuredArrow.map_mk, toCostructuredArrow_obj, Functor.op_obj,
  Functor.comp_obj]
case h_obj.e_f
C : Type u
inst✝ : Category C
F : C ⥤ Type w
F₁ F₂ : Cᵒᵖ ⥤ Type v
α : F₁ ⟶ F₂
X : (Functor.Elements F₁)ᵒᵖ
⊢ (yonedaSections ((map α).obj X.unop).op.unop.fst.unop F₂).inv { down := ((map α).obj X.unop).op.unop.snd } =
    (yonedaSections X.unop.fst.unop F₁).inv { down := X.unop.snd } ≫ α
case h_obj
C : Type u
inst✝ : Category C
F : C ⥤ Type w
F₁ F₂ : Cᵒᵖ ⥤ Type v
α : F₁ ⟶ F₂
X : (Functor.Elements F₁)ᵒᵖ
⊢ CostructuredArrow.mk
      ((yonedaSections ((map α).obj X.unop).op.unop.fst.unop F₂).inv { down := ((map α).obj X.unop).op.unop.snd }) =
    CostructuredArrow.mk ((yonedaSections X.unop.fst.unop F₁).inv { down := X.unop.snd } ≫ α)
congr
case h_obj.e_f.w.h.h
C : Type u
inst✝ : Category C
F : C ⥤ Type w
F₁ F₂ : Cᵒᵖ ⥤ Type v
α : F₁ ⟶ F₂
X : (Functor.Elements F₁)ᵒᵖ
x✝ : Cᵒᵖ
f : (yoneda.obj ((map α).obj X.unop).op.unop.fst.unop).obj x✝
⊢ ((yonedaSections ((map α).obj X.unop).op.unop.fst.unop F₂).inv { down := ((map α).obj X.unop).op.unop.snd }).app x✝
      f =
    ((yonedaSections X.unop.fst.unop F₁).inv { down := X.unop.snd } ≫ α).app x✝ f
case h_obj.e_f
C : Type u
inst✝ : Category C
F : C ⥤ Type w
F₁ F₂ : Cᵒᵖ ⥤ Type v
α : F₁ ⟶ F₂
X : (Functor.Elements F₁)ᵒᵖ
⊢ (yonedaSections ((map α).obj X.unop).op.unop.fst.unop F₂).inv { down := ((map α).obj X.unop).op.unop.snd } =
    (yonedaSections X.unop.fst.unop F₁).inv { down := X.unop.snd } ≫ α
ext _ f
no goals
case h_obj.e_f.w.h.h
C : Type u
inst✝ : Category C
F : C ⥤ Type w
F₁ F₂ : Cᵒᵖ ⥤ Type v
α : F₁ ⟶ F₂
X : (Functor.Elements F₁)ᵒᵖ
x✝ : Cᵒᵖ
f : (yoneda.obj ((map α).obj X.unop).op.unop.fst.unop).obj x✝
⊢ ((yonedaSections ((map α).obj X.unop).op.unop.fst.unop F₂).inv { down := ((map α).obj X.unop).op.unop.snd }).app x✝
      f =
    ((yonedaSections X.unop.fst.unop F₁).inv { down := X.unop.snd } ≫ α).app x✝ f
simpa using congr_fun (α.naturality f.op).symm (unop X).snd
case h_map
C : Type u
inst✝ : Category C
F : C ⥤ Type w
F₁ F₂ : Cᵒᵖ ⥤ Type v
α : F₁ ⟶ F₂
X Y : (Functor.Elements F₁)ᵒᵖ
f : X ⟶ Y
⊢ (Functor.op (map α) ⋙ toCostructuredArrow F₂).map f =
    eqToHom
        (_ :
          (Functor.op (map α) ⋙ toCostructuredArrow F₂).obj X =
            (toCostructuredArrow F₁ ⋙ CostructuredArrow.map α).obj X) ≫
      (toCostructuredArrow F₁ ⋙ CostructuredArrow.map α).map f ≫
        eqToHom
          (_ :
            (toCostructuredArrow F₁ ⋙ CostructuredArrow.map α).obj Y =
              (Functor.op (map α) ⋙ toCostructuredArrow F₂).obj Y)
case h_map
C : Type u
inst✝ : Category C
F : C ⥤ Type w
F₁ F₂ : Cᵒᵖ ⥤ Type v
α : F₁ ⟶ F₂
⊢ autoParam
    (∀ (X Y : (Functor.Elements F₁)ᵒᵖ) (f : X ⟶ Y),
      (Functor.op (map α) ⋙ toCostructuredArrow F₂).map f =
        eqToHom
            (_ :
              (Functor.op (map α) ⋙ toCostructuredArrow F₂).obj X =
                (toCostructuredArrow F₁ ⋙ CostructuredArrow.map α).obj X) ≫
          (toCostructuredArrow F₁ ⋙ CostructuredArrow.map α).map f ≫
            eqToHom
              (_ :
                (toCostructuredArrow F₁ ⋙ CostructuredArrow.map α).obj Y =
                  (Functor.op (map α) ⋙ toCostructuredArrow F₂).obj Y))
    _auto✝
intro X Y f
case h_map.h
C : Type u
inst✝ : Category C
F : C ⥤ Type w
F₁ F₂ : Cᵒᵖ ⥤ Type v
α : F₁ ⟶ F₂
X Y : (Functor.Elements F₁)ᵒᵖ
f : X ⟶ Y
⊢ ((Functor.op (map α) ⋙ toCostructuredArrow F₂).map f).left =
    (eqToHom
          (_ :
            (Functor.op (map α) ⋙ toCostructuredArrow F₂).obj X =
              (toCostructuredArrow F₁ ⋙ CostructuredArrow.map α).obj X) ≫
        (toCostructuredArrow F₁ ⋙ CostructuredArrow.map α).map f ≫
          eqToHom
            (_ :
              (toCostructuredArrow F₁ ⋙ CostructuredArrow.map α).obj Y =
                (Functor.op (map α) ⋙ toCostructuredArrow F₂).obj Y)).left
case h_map
C : Type u
inst✝ : Category C
F : C ⥤ Type w
F₁ F₂ : Cᵒᵖ ⥤ Type v
α : F₁ ⟶ F₂
X Y : (Functor.Elements F₁)ᵒᵖ
f : X ⟶ Y
⊢ (Functor.op (map α) ⋙ toCostructuredArrow F₂).map f =
    eqToHom
        (_ :
          (Functor.op (map α) ⋙ toCostructuredArrow F₂).obj X =
            (toCostructuredArrow F₁ ⋙ CostructuredArrow.map α).obj X) ≫
      (toCostructuredArrow F₁ ⋙ CostructuredArrow.map α).map f ≫
        eqToHom
          (_ :
            (toCostructuredArrow F₁ ⋙ CostructuredArrow.map α).obj Y =
              (Functor.op (map α) ⋙ toCostructuredArrow F₂).obj Y)
ext
no goals
case h_map.h
C : Type u
inst✝ : Category C
F : C ⥤ Type w
F₁ F₂ : Cᵒᵖ ⥤ Type v
α : F₁ ⟶ F₂
X Y : (Functor.Elements F₁)ᵒᵖ
f : X ⟶ Y
⊢ ((Functor.op (map α) ⋙ toCostructuredArrow F₂).map f).left =
    (eqToHom
          (_ :
            (Functor.op (map α) ⋙ toCostructuredArrow F₂).obj X =
              (toCostructuredArrow F₁ ⋙ CostructuredArrow.map α).obj X) ≫
        (toCostructuredArrow F₁ ⋙ CostructuredArrow.map α).map f ≫
          eqToHom
            (_ :
              (toCostructuredArrow F₁ ⋙ CostructuredArrow.map α).obj Y =
                (Functor.op (map α) ⋙ toCostructuredArrow F₂).obj Y)).left
simp [CostructuredArrow.eqToHom_left]