case refine'_1
C : Type u
inst✝ : Category C
F✝ : C ⥤ Type w
F : Cᵒᵖ ⥤ Type v
⊢ ∀ (X : CostructuredArrow yoneda F),
    ((fromCostructuredArrow F).rightOp ⋙ toCostructuredArrow F).obj X = (𝟭 (CostructuredArrow yoneda F)).obj X

case refine'_2
C : Type u
inst✝ : Category C
F✝ : C ⥤ Type w
F : Cᵒᵖ ⥤ Type v
⊢ ∀ (X Y : CostructuredArrow yoneda F) (f : X ⟶ Y),
    ((fromCostructuredArrow F).rightOp ⋙ toCostructuredArrow F).map f =
      eqToHom (_ : ?m.87063.obj X = ?m.87064.obj X) ≫
        (𝟭 (CostructuredArrow yoneda F)).map f ≫
          eqToHom
            (_ :
              (𝟭 (CostructuredArrow yoneda F)).obj Y =
                ((fromCostructuredArrow F).rightOp ⋙ toCostructuredArrow F).obj Y)
C : Type u
inst✝ : Category C
F✝ : C ⥤ Type w
F : Cᵒᵖ ⥤ Type v
⊢ (fromCostructuredArrow F).rightOp ⋙ toCostructuredArrow F = 𝟭 (CostructuredArrow yoneda F)
refine' Functor.ext _ _
case refine'_1
C : Type u
inst✝ : Category C
F✝ : C ⥤ Type w
F : Cᵒᵖ ⥤ Type v
X : CostructuredArrow yoneda F
⊢ ((fromCostructuredArrow F).rightOp ⋙ toCostructuredArrow F).obj X = (𝟭 (CostructuredArrow yoneda F)).obj X
case refine'_1
C : Type u
inst✝ : Category C
F✝ : C ⥤ Type w
F : Cᵒᵖ ⥤ Type v
⊢ ∀ (X : CostructuredArrow yoneda F),
    ((fromCostructuredArrow F).rightOp ⋙ toCostructuredArrow F).obj X = (𝟭 (CostructuredArrow yoneda F)).obj X
intro X
case refine'_1.mk
C : Type u
inst✝ : Category C
F✝ : C ⥤ Type w
F : Cᵒᵖ ⥤ Type v
X_left : C
X_right : Discrete PUnit
X_hom : yoneda.obj X_left ⟶ (Functor.fromPUnit F).obj X_right
⊢ ((fromCostructuredArrow F).rightOp ⋙ toCostructuredArrow F).obj { left := X_left, right := X_right, hom := X_hom } =
    (𝟭 (CostructuredArrow yoneda F)).obj { left := X_left, right := X_right, hom := X_hom }
case refine'_1
C : Type u
inst✝ : Category C
F✝ : C ⥤ Type w
F : Cᵒᵖ ⥤ Type v
X : CostructuredArrow yoneda F
⊢ ((fromCostructuredArrow F).rightOp ⋙ toCostructuredArrow F).obj X = (𝟭 (CostructuredArrow yoneda F)).obj X
cases' X with X_left X_right X_hom
case refine'_1.mk.mk
C : Type u
inst✝ : Category C
F✝ : C ⥤ Type w
F : Cᵒᵖ ⥤ Type v
X_left : C
as✝ : PUnit
X_hom : yoneda.obj X_left ⟶ (Functor.fromPUnit F).obj { as := as✝ }
⊢ ((fromCostructuredArrow F).rightOp ⋙ toCostructuredArrow F).obj
      { left := X_left, right := { as := as✝ }, hom := X_hom } =
    (𝟭 (CostructuredArrow yoneda F)).obj { left := X_left, right := { as := as✝ }, hom := X_hom }
case refine'_1.mk
C : Type u
inst✝ : Category C
F✝ : C ⥤ Type w
F : Cᵒᵖ ⥤ Type v
X_left : C
X_right : Discrete PUnit
X_hom : yoneda.obj X_left ⟶ (Functor.fromPUnit F).obj X_right
⊢ ((fromCostructuredArrow F).rightOp ⋙ toCostructuredArrow F).obj { left := X_left, right := X_right, hom := X_hom } =
    (𝟭 (CostructuredArrow yoneda F)).obj { left := X_left, right := X_right, hom := X_hom }
cases X_right
case refine'_1.mk.mk
C : Type u
inst✝ : Category C
F✝ : C ⥤ Type w
F : Cᵒᵖ ⥤ Type v
X_left : C
as✝ : PUnit
X_hom : yoneda.obj X_left ⟶ (Functor.fromPUnit F).obj { as := as✝ }
⊢ {
      left :=
        ((fromCostructuredArrow F).obj { left := X_left, right := { as := as✝ }, hom := X_hom }.op).op.unop.fst.unop,
      right := { as := PUnit.unit },
      hom :=
        (yonedaSections
              ((fromCostructuredArrow F).obj
                        { left := X_left, right := { as := as✝ }, hom := X_hom }.op).op.unop.fst.unop
              F).inv
          {
            down :=
              ((fromCostructuredArrow F).obj
                      { left := X_left, right := { as := as✝ }, hom := X_hom }.op).op.unop.snd } } =
    { left := X_left, right := { as := as✝ }, hom := X_hom }
case refine'_1.mk.mk
C : Type u
inst✝ : Category C
F✝ : C ⥤ Type w
F : Cᵒᵖ ⥤ Type v
X_left : C
as✝ : PUnit
X_hom : yoneda.obj X_left ⟶ (Functor.fromPUnit F).obj { as := as✝ }
⊢ ((fromCostructuredArrow F).rightOp ⋙ toCostructuredArrow F).obj
      { left := X_left, right := { as := as✝ }, hom := X_hom } =
    (𝟭 (CostructuredArrow yoneda F)).obj { left := X_left, right := { as := as✝ }, hom := X_hom }
simp only [Functor.id_obj, Functor.rightOp_obj, toCostructuredArrow_obj, Functor.comp_obj,
  CostructuredArrow.mk]
case refine'_1.mk.mk.e_hom
C : Type u
inst✝ : Category C
F✝ : C ⥤ Type w
F : Cᵒᵖ ⥤ Type v
X_left : C
as✝ : PUnit
X_hom : yoneda.obj X_left ⟶ (Functor.fromPUnit F).obj { as := as✝ }
⊢ (yonedaSections
          ((fromCostructuredArrow F).obj { left := X_left, right := { as := as✝ }, hom := X_hom }.op).op.unop.fst.unop
          F).inv
      {
        down :=
          ((fromCostructuredArrow F).obj { left := X_left, right := { as := as✝ }, hom := X_hom }.op).op.unop.snd } =
    X_hom
case refine'_1.mk.mk
C : Type u
inst✝ : Category C
F✝ : C ⥤ Type w
F : Cᵒᵖ ⥤ Type v
X_left : C
as✝ : PUnit
X_hom : yoneda.obj X_left ⟶ (Functor.fromPUnit F).obj { as := as✝ }
⊢ {
      left :=
        ((fromCostructuredArrow F).obj { left := X_left, right := { as := as✝ }, hom := X_hom }.op).op.unop.fst.unop,
      right := { as := PUnit.unit },
      hom :=
        (yonedaSections
              ((fromCostructuredArrow F).obj
                        { left := X_left, right := { as := as✝ }, hom := X_hom }.op).op.unop.fst.unop
              F).inv
          {
            down :=
              ((fromCostructuredArrow F).obj
                      { left := X_left, right := { as := as✝ }, hom := X_hom }.op).op.unop.snd } } =
    { left := X_left, right := { as := as✝ }, hom := X_hom }
congr
case refine'_1.mk.mk.e_hom.w.h.h
C : Type u
inst✝ : Category C
F✝ : C ⥤ Type w
F : Cᵒᵖ ⥤ Type v
X_left : C
as✝ : PUnit
X_hom : yoneda.obj X_left ⟶ (Functor.fromPUnit F).obj { as := as✝ }
x : Cᵒᵖ
f :
  (yoneda.obj
        ((fromCostructuredArrow F).obj
                  { left := X_left, right := { as := as✝ }, hom := X_hom }.op).op.unop.fst.unop).obj
    x
⊢ ((yonedaSections
              ((fromCostructuredArrow F).obj
                        { left := X_left, right := { as := as✝ }, hom := X_hom }.op).op.unop.fst.unop
              F).inv
          {
            down :=
              ((fromCostructuredArrow F).obj
                      { left := X_left, right := { as := as✝ }, hom := X_hom }.op).op.unop.snd }).app
      x f =
    X_hom.app x f
case refine'_1.mk.mk.e_hom
C : Type u
inst✝ : Category C
F✝ : C ⥤ Type w
F : Cᵒᵖ ⥤ Type v
X_left : C
as✝ : PUnit
X_hom : yoneda.obj X_left ⟶ (Functor.fromPUnit F).obj { as := as✝ }
⊢ (yonedaSections
          ((fromCostructuredArrow F).obj { left := X_left, right := { as := as✝ }, hom := X_hom }.op).op.unop.fst.unop
          F).inv
      {
        down :=
          ((fromCostructuredArrow F).obj { left := X_left, right := { as := as✝ }, hom := X_hom }.op).op.unop.snd } =
    X_hom
ext x f
case h.e'_3.h
C : Type u
inst✝ : Category C
F✝ : C ⥤ Type w
F : Cᵒᵖ ⥤ Type v
X_left : C
as✝ : PUnit
X_hom : yoneda.obj X_left ⟶ (Functor.fromPUnit F).obj { as := as✝ }
x : Cᵒᵖ
f :
  (yoneda.obj
        ((fromCostructuredArrow F).obj
                  { left := X_left, right := { as := as✝ }, hom := X_hom }.op).op.unop.fst.unop).obj
    x
e_1✝ : F.obj x = ((Functor.fromPUnit F).obj { as := as✝ }).obj x.unop.op
⊢ X_hom.app x f = ((yoneda.obj X_left).map f.op ≫ X_hom.app x.unop.op) (𝟙 X_left)
case refine'_1.mk.mk.e_hom.w.h.h
C : Type u
inst✝ : Category C
F✝ : C ⥤ Type w
F : Cᵒᵖ ⥤ Type v
X_left : C
as✝ : PUnit
X_hom : yoneda.obj X_left ⟶ (Functor.fromPUnit F).obj { as := as✝ }
x : Cᵒᵖ
f :
  (yoneda.obj
        ((fromCostructuredArrow F).obj
                  { left := X_left, right := { as := as✝ }, hom := X_hom }.op).op.unop.fst.unop).obj
    x
⊢ ((yonedaSections
              ((fromCostructuredArrow F).obj
                        { left := X_left, right := { as := as✝ }, hom := X_hom }.op).op.unop.fst.unop
              F).inv
          {
            down :=
              ((fromCostructuredArrow F).obj
                      { left := X_left, right := { as := as✝ }, hom := X_hom }.op).op.unop.snd }).app
      x f =
    X_hom.app x f
convert congr_fun (X_hom.naturality f.op).symm (𝟙 X_left)
no goals
case h.e'_3.h
C : Type u
inst✝ : Category C
F✝ : C ⥤ Type w
F : Cᵒᵖ ⥤ Type v
X_left : C
as✝ : PUnit
X_hom : yoneda.obj X_left ⟶ (Functor.fromPUnit F).obj { as := as✝ }
x : Cᵒᵖ
f :
  (yoneda.obj
        ((fromCostructuredArrow F).obj
                  { left := X_left, right := { as := as✝ }, hom := X_hom }.op).op.unop.fst.unop).obj
    x
e_1✝ : F.obj x = ((Functor.fromPUnit F).obj { as := as✝ }).obj x.unop.op
⊢ X_hom.app x f = ((yoneda.obj X_left).map f.op ≫ X_hom.app x.unop.op) (𝟙 X_left)
simp
case refine'_2
C : Type u
inst✝ : Category C
F✝ : C ⥤ Type w
F : Cᵒᵖ ⥤ Type v
X Y : CostructuredArrow yoneda F
f : X ⟶ Y
⊢ ((fromCostructuredArrow F).rightOp ⋙ toCostructuredArrow F).map f =
    eqToHom
        (_ :
          ((fromCostructuredArrow F).rightOp ⋙ toCostructuredArrow F).obj X = (𝟭 (CostructuredArrow yoneda F)).obj X) ≫
      (𝟭 (CostructuredArrow yoneda F)).map f ≫
        eqToHom
          (_ :
            (𝟭 (CostructuredArrow yoneda F)).obj Y = ((fromCostructuredArrow F).rightOp ⋙ toCostructuredArrow F).obj Y)
case refine'_2
C : Type u
inst✝ : Category C
F✝ : C ⥤ Type w
F : Cᵒᵖ ⥤ Type v
⊢ ∀ (X Y : CostructuredArrow yoneda F) (f : X ⟶ Y),
    ((fromCostructuredArrow F).rightOp ⋙ toCostructuredArrow F).map f =
      eqToHom
          (_ :
            ((fromCostructuredArrow F).rightOp ⋙ toCostructuredArrow F).obj X =
              (𝟭 (CostructuredArrow yoneda F)).obj X) ≫
        (𝟭 (CostructuredArrow yoneda F)).map f ≫
          eqToHom
            (_ :
              (𝟭 (CostructuredArrow yoneda F)).obj Y =
                ((fromCostructuredArrow F).rightOp ⋙ toCostructuredArrow F).obj Y)
intro X Y f
case refine'_2.h
C : Type u
inst✝ : Category C
F✝ : C ⥤ Type w
F : Cᵒᵖ ⥤ Type v
X Y : CostructuredArrow yoneda F
f : X ⟶ Y
⊢ (((fromCostructuredArrow F).rightOp ⋙ toCostructuredArrow F).map f).left =
    (eqToHom
          (_ :
            ((fromCostructuredArrow F).rightOp ⋙ toCostructuredArrow F).obj X =
              (𝟭 (CostructuredArrow yoneda F)).obj X) ≫
        (𝟭 (CostructuredArrow yoneda F)).map f ≫
          eqToHom
            (_ :
              (𝟭 (CostructuredArrow yoneda F)).obj Y =
                ((fromCostructuredArrow F).rightOp ⋙ toCostructuredArrow F).obj Y)).left
case refine'_2
C : Type u
inst✝ : Category C
F✝ : C ⥤ Type w
F : Cᵒᵖ ⥤ Type v
X Y : CostructuredArrow yoneda F
f : X ⟶ Y
⊢ ((fromCostructuredArrow F).rightOp ⋙ toCostructuredArrow F).map f =
    eqToHom
        (_ :
          ((fromCostructuredArrow F).rightOp ⋙ toCostructuredArrow F).obj X = (𝟭 (CostructuredArrow yoneda F)).obj X) ≫
      (𝟭 (CostructuredArrow yoneda F)).map f ≫
        eqToHom
          (_ :
            (𝟭 (CostructuredArrow yoneda F)).obj Y = ((fromCostructuredArrow F).rightOp ⋙ toCostructuredArrow F).obj Y)
ext
no goals
case refine'_2.h
C : Type u
inst✝ : Category C
F✝ : C ⥤ Type w
F : Cᵒᵖ ⥤ Type v
X Y : CostructuredArrow yoneda F
f : X ⟶ Y
⊢ (((fromCostructuredArrow F).rightOp ⋙ toCostructuredArrow F).map f).left =
    (eqToHom
          (_ :
            ((fromCostructuredArrow F).rightOp ⋙ toCostructuredArrow F).obj X =
              (𝟭 (CostructuredArrow yoneda F)).obj X) ≫
        (𝟭 (CostructuredArrow yoneda F)).map f ≫
          eqToHom
            (_ :
              (𝟭 (CostructuredArrow yoneda F)).obj Y =
                ((fromCostructuredArrow F).rightOp ⋙ toCostructuredArrow F).obj Y)).left
simp [CostructuredArrow.eqToHom_left]