Final functors between intervals

instance Set.Ici.subtype_functor_final {J : Type u} [LinearOrder J] (j : J) : ⋯.functor.Final