∀ {J : Type u} {inst : LinearOrder J} {inst_1 : SuccOrder J} {F : CategoryTheory.Functor Jᵒᵖ (Type v)}
  {succ : (j : J) → ¬IsMax j → F.obj (Opposite.op j) → F.obj (Opposite.op (Order.succ j))}
  {map_succ :
    ∀ (j : J) (hj : ¬IsMax j) (x : F.obj (Opposite.op j)), F.map (CategoryTheory.homOfLE ⋯).op (succ j hj x) = x}
  {lift : (j : J) → Order.IsSuccLimit j → ↑(⋯.functor.op.comp F).sections → F.obj (Opposite.op j)}
  {map_lift :
    ∀ (j : J) (hj : Order.IsSuccLimit j) (x : ↑(⋯.functor.op.comp F).sections) (i : J) (hi : i < j),
      F.map (CategoryTheory.homOfLE ⋯).op (lift j hj x) = ↑x (Opposite.op ⟨i, hi⟩)}
  {succ_1 : (j : J) → ¬IsMax j → F.obj (Opposite.op j) → F.obj (Opposite.op (Order.succ j))}
  {map_succ_1 :
    ∀ (j : J) (hj : ¬IsMax j) (x : F.obj (Opposite.op j)), F.map (CategoryTheory.homOfLE ⋯).op (succ_1 j hj x) = x}
  {lift_1 : (j : J) → Order.IsSuccLimit j → ↑(⋯.functor.op.comp F).sections → F.obj (Opposite.op j)}
  {map_lift_1 :
    ∀ (j : J) (hj : Order.IsSuccLimit j) (x : ↑(⋯.functor.op.comp F).sections) (i : J) (hi : i < j),
      F.map (CategoryTheory.homOfLE ⋯).op (lift_1 j hj x) = ↑x (Opposite.op ⟨i, hi⟩)},
  { succ := succ, map_succ := map_succ, lift := lift, map_lift := map_lift } =
      { succ := succ_1, map_succ := map_succ_1, lift := lift_1, map_lift := map_lift_1 } →
    succ = succ_1 ∧ lift = lift_1