Inverse order `nonempty_sections_of_fintype_inverse_system`

Stream: new members

[Rémi Bottinelli]

Hi,

I want to use nonempty_sections_of_fintype_inverse_system but drop the opposite part.
I've tried the following, but get an error on the line have F'sections_nempty : F'.sections.nonempty := nonempty_sections_of_fintype_inverse_system F',.

import category_theory.filtered
import topology.category.Top.limits
import category_theory.category.basic
import category_theory.full_subcategory
import data.opposite


universes u v w

open classical
open category_theory

noncomputable theory
local attribute [instance] prop_decidable



variables {J : Type u} [preorder J] [is_directed J ge] (F : J ⥤ Type v)


instance Joppreo : preorder Jᵒᵖ := {
  le := λ jop jop', jop'.unop ≤ jop.unop,
  lt := λ jop jop', jop'.unop < jop.unop,
  le_refl := λ jop, preorder.le_refl jop.unop,
  le_trans := λ j₁ j₂ j₃, λ h₁₂ h₂₃, preorder.le_trans _ _ _ h₂₃ h₁₂,
  lt_iff_le_not_le := λ j₁ j₂, preorder.lt_iff_le_not_le j₂.unop j₁.unop
  }

instance Jopdir  : is_directed Jᵒᵖ (≤) :=
{ directed := λ jop jop', by
  { obtain ⟨c,cj,cj'⟩ := directed_of (ge) jop.unop jop'.unop,
    use opposite.op c, rw ←opposite.unop_op c at cj cj',
    exact ⟨cj,cj'⟩,}}


theorem nonempty_sections_of_fintype_inverse_system'
 [fin : Π (j : J), fintype (F.obj j)] [nempty : ∀ (j : J), nonempty (F.obj j)] : F.sections.nonempty :=
begin
  let F' : (Jᵒᵖ)ᵒᵖ ⥤ Type v := (category_theory.op_op J).comp F,
  haveI fin' : Π j : (Jᵒᵖ)ᵒᵖ, fintype (F'.obj j) := λ jopop, by {apply fin,},
  haveI nempty' : ∀ j : (Jᵒᵖ)ᵒᵖ, nonempty (F'.obj j) := λ jopop, by {apply nempty,},
  have F'sections_nempty : F'.sections.nonempty := nonempty_sections_of_fintype_inverse_system F',
  obtain ⟨s,sec⟩ := F'sections_nempty,
  fapply Exists.intro,
  exact λ j, s (opposite.op $ opposite.op j),
  exact λ j j' f, @sec (opposite.op $ opposite.op j)(opposite.op $ opposite.op j') (f.op.op),
end

After some investigation, I get a more useful error message:

type mismatch at application
  nonempty_sections_of_fintype_inverse_system F'
term
  F'
has type
  @category_theory.functor (opposite (opposite J))
    (@category_theory.category.opposite (opposite J)
       (@category_theory.category.opposite J (@preorder.small_category J _inst_1)))
    (Type v)
    category_theory.types
but is expected to have type
  @category_theory.functor (opposite (opposite J))
    (@category_theory.category.opposite (opposite J)
       (@preorder.small_category (opposite J) (@inverse_system.Joppreo J _inst_1 _inst_2)))
    (Type v)
    category_theory.types

I believe this is due to having a few different ways to do different constructions, but am not sure exactly where the problem lies, nor how to solve it.
Any idea? Thanks!