J : Type u
inst✝³ : Category J
inst✝² : IsCofilteredOrEmpty J
F : J ⥤ Type v
inst✝¹ : ∀ (j : J), Finite (F.obj j)
inst✝ : ∀ (j : J), _root_.Nonempty (F.obj j)
J' : Type (max w v u) := AsSmall J
⊢ Set.Nonempty (Functor.sections F)
J : Type u
inst✝³ : Category J
inst✝² : IsCofilteredOrEmpty J
F : J ⥤ Type v
inst✝¹ : ∀ (j : J), Finite (F.obj j)
inst✝ : ∀ (j : J), _root_.Nonempty (F.obj j)
⊢ Set.Nonempty (Functor.sections F)
let J' : Type max w v u := AsSmall.{max w v} J
J : Type u
inst✝³ : Category J
inst✝² : IsCofilteredOrEmpty J
F : J ⥤ Type v
inst✝¹ : ∀ (j : J), Finite (F.obj j)
inst✝ : ∀ (j : J), _root_.Nonempty (F.obj j)
J' : Type (max w v u) := AsSmall J
down : J' ⥤ J := AsSmall.down
⊢ Set.Nonempty (Functor.sections F)
J : Type u
inst✝³ : Category J
inst✝² : IsCofilteredOrEmpty J
F : J ⥤ Type v
inst✝¹ : ∀ (j : J), Finite (F.obj j)
inst✝ : ∀ (j : J), _root_.Nonempty (F.obj j)
J' : Type (max w v u) := AsSmall J
⊢ Set.Nonempty (Functor.sections F)
let down : J' ⥤ J := AsSmall.down
J : Type u
inst✝³ : Category J
inst✝² : IsCofilteredOrEmpty J
F : J ⥤ Type v
inst✝¹ : ∀ (j : J), Finite (F.obj j)
inst✝ : ∀ (j : J), _root_.Nonempty (F.obj j)
J' : Type (max w v u) := AsSmall J
down : J' ⥤ J := AsSmall.down
F' : J' ⥤ Type (max u v w) := down ⋙ F ⋙ uliftFunctor
⊢ Set.Nonempty (Functor.sections F)
J : Type u
inst✝³ : Category J
inst✝² : IsCofilteredOrEmpty J
F : J ⥤ Type v
inst✝¹ : ∀ (j : J), Finite (F.obj j)
inst✝ : ∀ (j : J), _root_.Nonempty (F.obj j)
J' : Type (max w v u) := AsSmall J
down : J' ⥤ J := AsSmall.down
⊢ Set.Nonempty (Functor.sections F)
let F' : J' ⥤ Type max u v w := down ⋙ F ⋙ uliftFunctor.{max u w, v}
J : Type u
inst✝³ : Category J
inst✝² : IsCofilteredOrEmpty J
F : J ⥤ Type v
inst✝¹ : ∀ (j : J), Finite (F.obj j)
inst✝ : ∀ (j : J), _root_.Nonempty (F.obj j)
J' : Type (max w v u) := AsSmall J
down : J' ⥤ J := AsSmall.down
F' : J' ⥤ Type (max u v w) := down ⋙ F ⋙ uliftFunctor
this : ∀ (i : J'), _root_.Nonempty (F'.obj i)
⊢ Set.Nonempty (Functor.sections F)
J : Type u
inst✝³ : Category J
inst✝² : IsCofilteredOrEmpty J
F : J ⥤ Type v
inst✝¹ : ∀ (j : J), Finite (F.obj j)
inst✝ : ∀ (j : J), _root_.Nonempty (F.obj j)
J' : Type (max w v u) := AsSmall J
down : J' ⥤ J := AsSmall.down
F' : J' ⥤ Type (max u v w) := down ⋙ F ⋙ uliftFunctor
⊢ Set.Nonempty (Functor.sections F)
haveI : ∀ i, Nonempty (F'.obj i) := fun i => ⟨⟨Classical.arbitrary (F.obj (down.obj i))⟩⟩
J : Type u
inst✝³ : Category J
inst✝² : IsCofilteredOrEmpty J
F : J ⥤ Type v
inst✝¹ : ∀ (j : J), Finite (F.obj j)
inst✝ : ∀ (j : J), _root_.Nonempty (F.obj j)
J' : Type (max w v u) := AsSmall J
down : J' ⥤ J := AsSmall.down
F' : J' ⥤ Type (max u v w) := down ⋙ F ⋙ uliftFunctor
this✝ : ∀ (i : J'), _root_.Nonempty (F'.obj i)
this : ∀ (i : J'), Finite (F'.obj i)
⊢ Set.Nonempty (Functor.sections F)
J : Type u
inst✝³ : Category J
inst✝² : IsCofilteredOrEmpty J
F : J ⥤ Type v
inst✝¹ : ∀ (j : J), Finite (F.obj j)
inst✝ : ∀ (j : J), _root_.Nonempty (F.obj j)
J' : Type (max w v u) := AsSmall J
down : J' ⥤ J := AsSmall.down
F' : J' ⥤ Type (max u v w) := down ⋙ F ⋙ uliftFunctor
this : ∀ (i : J'), _root_.Nonempty (F'.obj i)
⊢ Set.Nonempty (Functor.sections F)
haveI : ∀ i, Finite (F'.obj i) := fun i => Finite.of_equiv (F.obj (down.obj i)) Equiv.ulift.symm
case inl
J : Type u
inst✝³ : Category J
inst✝² : IsCofilteredOrEmpty J
F : J ⥤ Type v
inst✝¹ : ∀ (j : J), Finite (F.obj j)
inst✝ : ∀ (j : J), _root_.Nonempty (F.obj j)
J' : Type (max w v u) := AsSmall J
down : J' ⥤ J := AsSmall.down
F' : J' ⥤ Type (max u v w) := down ⋙ F ⋙ uliftFunctor
this✝ : ∀ (i : J'), _root_.Nonempty (F'.obj i)
this : ∀ (i : J'), Finite (F'.obj i)
h✝ : IsEmpty J
⊢ Set.Nonempty (Functor.sections F)

case inr
J : Type u
inst✝³ : Category J
inst✝² : IsCofilteredOrEmpty J
F : J ⥤ Type v
inst✝¹ : ∀ (j : J), Finite (F.obj j)
inst✝ : ∀ (j : J), _root_.Nonempty (F.obj j)
J' : Type (max w v u) := AsSmall J
down : J' ⥤ J := AsSmall.down
F' : J' ⥤ Type (max u v w) := down ⋙ F ⋙ uliftFunctor
this✝ : ∀ (i : J'), _root_.Nonempty (F'.obj i)
this : ∀ (i : J'), Finite (F'.obj i)
h✝ : _root_.Nonempty J
⊢ Set.Nonempty (Functor.sections F)
J : Type u
inst✝³ : Category J
inst✝² : IsCofilteredOrEmpty J
F : J ⥤ Type v
inst✝¹ : ∀ (j : J), Finite (F.obj j)
inst✝ : ∀ (j : J), _root_.Nonempty (F.obj j)
J' : Type (max w v u) := AsSmall J
down : J' ⥤ J := AsSmall.down
F' : J' ⥤ Type (max u v w) := down ⋙ F ⋙ uliftFunctor
this✝ : ∀ (i : J'), _root_.Nonempty (F'.obj i)
this : ∀ (i : J'), Finite (F'.obj i)
⊢ Set.Nonempty (Functor.sections F)
cases isEmpty_or_nonempty J
case inr
J : Type u
inst✝³ : Category J
inst✝² : IsCofilteredOrEmpty J
F : J ⥤ Type v
inst✝¹ : ∀ (j : J), Finite (F.obj j)
inst✝ : ∀ (j : J), _root_.Nonempty (F.obj j)
J' : Type (max w v u) := AsSmall J
down : J' ⥤ J := AsSmall.down
F' : J' ⥤ Type (max u v w) := down ⋙ F ⋙ uliftFunctor
this✝¹ : ∀ (i : J'), _root_.Nonempty (F'.obj i)
this✝ : ∀ (i : J'), Finite (F'.obj i)
h✝ : _root_.Nonempty J
this : IsCofiltered J
⊢ Set.Nonempty (Functor.sections F)
case inr
J : Type u
inst✝³ : Category J
inst✝² : IsCofilteredOrEmpty J
F : J ⥤ Type v
inst✝¹ : ∀ (j : J), Finite (F.obj j)
inst✝ : ∀ (j : J), _root_.Nonempty (F.obj j)
J' : Type (max w v u) := AsSmall J
down : J' ⥤ J := AsSmall.down
F' : J' ⥤ Type (max u v w) := down ⋙ F ⋙ uliftFunctor
this✝ : ∀ (i : J'), _root_.Nonempty (F'.obj i)
this : ∀ (i : J'), Finite (F'.obj i)
h✝ : _root_.Nonempty J
⊢ Set.Nonempty (Functor.sections F)
haveI : IsCofiltered J := ⟨⟩
case inr.intro
J : Type u
inst✝³ : Category J
inst✝² : IsCofilteredOrEmpty J
F : J ⥤ Type v
inst✝¹ : ∀ (j : J), Finite (F.obj j)
inst✝ : ∀ (j : J), _root_.Nonempty (F.obj j)
J' : Type (max w v u) := AsSmall J
down : J' ⥤ J := AsSmall.down
F' : J' ⥤ Type (max u v w) := down ⋙ F ⋙ uliftFunctor
this✝¹ : ∀ (i : J'), _root_.Nonempty (F'.obj i)
this✝ : ∀ (i : J'), Finite (F'.obj i)
h✝ : _root_.Nonempty J
this : IsCofiltered J
u : (j : J') → F'.obj j
hu : u ∈ Functor.sections F'
⊢ Set.Nonempty (Functor.sections F)
case inr
J : Type u
inst✝³ : Category J
inst✝² : IsCofilteredOrEmpty J
F : J ⥤ Type v
inst✝¹ : ∀ (j : J), Finite (F.obj j)
inst✝ : ∀ (j : J), _root_.Nonempty (F.obj j)
J' : Type (max w v u) := AsSmall J
down : J' ⥤ J := AsSmall.down
F' : J' ⥤ Type (max u v w) := down ⋙ F ⋙ uliftFunctor
this✝¹ : ∀ (i : J'), _root_.Nonempty (F'.obj i)
this✝ : ∀ (i : J'), Finite (F'.obj i)
h✝ : _root_.Nonempty J
this : IsCofiltered J
⊢ Set.Nonempty (Functor.sections F)
obtain ⟨u, hu⟩ := nonempty_sections_of_finite_cofiltered_system.init F'
case inr.intro
J : Type u
inst✝³ : Category J
inst✝² : IsCofilteredOrEmpty J
F : J ⥤ Type v
inst✝¹ : ∀ (j : J), Finite (F.obj j)
inst✝ : ∀ (j : J), _root_.Nonempty (F.obj j)
J' : Type (max w v u) := AsSmall J
down : J' ⥤ J := AsSmall.down
F' : J' ⥤ Type (max u v w) := down ⋙ F ⋙ uliftFunctor
this✝¹ : ∀ (i : J'), _root_.Nonempty (F'.obj i)
this✝ : ∀ (i : J'), Finite (F'.obj i)
h✝ : _root_.Nonempty J
this : IsCofiltered J
u : (j : J') → F'.obj j
hu : u ∈ Functor.sections F'
⊢ (fun j => (u { down := j }).down) ∈ Functor.sections F
case inr.intro
J : Type u
inst✝³ : Category J
inst✝² : IsCofilteredOrEmpty J
F : J ⥤ Type v
inst✝¹ : ∀ (j : J), Finite (F.obj j)
inst✝ : ∀ (j : J), _root_.Nonempty (F.obj j)
J' : Type (max w v u) := AsSmall J
down : J' ⥤ J := AsSmall.down
F' : J' ⥤ Type (max u v w) := down ⋙ F ⋙ uliftFunctor
this✝¹ : ∀ (i : J'), _root_.Nonempty (F'.obj i)
this✝ : ∀ (i : J'), Finite (F'.obj i)
h✝ : _root_.Nonempty J
this : IsCofiltered J
u : (j : J') → F'.obj j
hu : u ∈ Functor.sections F'
⊢ Set.Nonempty (Functor.sections F)
use fun j => (u ⟨j⟩).down
case inr.intro
J : Type u
inst✝³ : Category J
inst✝² : IsCofilteredOrEmpty J
F : J ⥤ Type v
inst✝¹ : ∀ (j : J), Finite (F.obj j)
inst✝ : ∀ (j : J), _root_.Nonempty (F.obj j)
J' : Type (max w v u) := AsSmall J
down : J' ⥤ J := AsSmall.down
F' : J' ⥤ Type (max u v w) := down ⋙ F ⋙ uliftFunctor
this✝¹ : ∀ (i : J'), _root_.Nonempty (F'.obj i)
this✝ : ∀ (i : J'), Finite (F'.obj i)
h✝ : _root_.Nonempty J
this : IsCofiltered J
u : (j : J') → F'.obj j
hu : u ∈ Functor.sections F'
j j' : J
f : j ⟶ j'
⊢ F.map f ((fun j => (u { down := j }).down) j) = (fun j => (u { down := j }).down) j'
case inr.intro
J : Type u
inst✝³ : Category J
inst✝² : IsCofilteredOrEmpty J
F : J ⥤ Type v
inst✝¹ : ∀ (j : J), Finite (F.obj j)
inst✝ : ∀ (j : J), _root_.Nonempty (F.obj j)
J' : Type (max w v u) := AsSmall J
down : J' ⥤ J := AsSmall.down
F' : J' ⥤ Type (max u v w) := down ⋙ F ⋙ uliftFunctor
this✝¹ : ∀ (i : J'), _root_.Nonempty (F'.obj i)
this✝ : ∀ (i : J'), Finite (F'.obj i)
h✝ : _root_.Nonempty J
this : IsCofiltered J
u : (j : J') → F'.obj j
hu : u ∈ Functor.sections F'
⊢ (fun j => (u { down := j }).down) ∈ Functor.sections F
intro j j' f
case inr.intro
J : Type u
inst✝³ : Category J
inst✝² : IsCofilteredOrEmpty J
F : J ⥤ Type v
inst✝¹ : ∀ (j : J), Finite (F.obj j)
inst✝ : ∀ (j : J), _root_.Nonempty (F.obj j)
J' : Type (max w v u) := AsSmall J
down : J' ⥤ J := AsSmall.down
F' : J' ⥤ Type (max u v w) := down ⋙ F ⋙ uliftFunctor
this✝¹ : ∀ (i : J'), _root_.Nonempty (F'.obj i)
this✝ : ∀ (i : J'), Finite (F'.obj i)
h✝ : _root_.Nonempty J
this : IsCofiltered J
u : (j : J') → F'.obj j
hu : u ∈ Functor.sections F'
j j' : J
f : j ⟶ j'
h : F'.map { down := f } (u { down := j }) = u { down := j' }
⊢ F.map f ((fun j => (u { down := j }).down) j) = (fun j => (u { down := j }).down) j'
case inr.intro
J : Type u
inst✝³ : Category J
inst✝² : IsCofilteredOrEmpty J
F : J ⥤ Type v
inst✝¹ : ∀ (j : J), Finite (F.obj j)
inst✝ : ∀ (j : J), _root_.Nonempty (F.obj j)
J' : Type (max w v u) := AsSmall J
down : J' ⥤ J := AsSmall.down
F' : J' ⥤ Type (max u v w) := down ⋙ F ⋙ uliftFunctor
this✝¹ : ∀ (i : J'), _root_.Nonempty (F'.obj i)
this✝ : ∀ (i : J'), Finite (F'.obj i)
h✝ : _root_.Nonempty J
this : IsCofiltered J
u : (j : J') → F'.obj j
hu : u ∈ Functor.sections F'
j j' : J
f : j ⟶ j'
⊢ F.map f ((fun j => (u { down := j }).down) j) = (fun j => (u { down := j }).down) j'
have h := @hu (⟨j⟩ : J') (⟨j'⟩ : J') (ULift.up f)
case inr.intro
J : Type u
inst✝³ : Category J
inst✝² : IsCofilteredOrEmpty J
F : J ⥤ Type v
inst✝¹ : ∀ (j : J), Finite (F.obj j)
inst✝ : ∀ (j : J), _root_.Nonempty (F.obj j)
J' : Type (max w v u) := AsSmall J
down : J' ⥤ J := AsSmall.down
F' : J' ⥤ Type (max u v w) := down ⋙ F ⋙ uliftFunctor
this✝¹ : ∀ (i : J'), _root_.Nonempty (F'.obj i)
this✝ : ∀ (i : J'), Finite (F'.obj i)
h✝ : _root_.Nonempty J
this : IsCofiltered J
u : (j : J') → F'.obj j
hu : u ∈ Functor.sections F'
j j' : J
f : j ⟶ j'
h : { down := F.map f (u { down := j }).down } = u { down := j' }
⊢ F.map f ((fun j => (u { down := j }).down) j) = (fun j => (u { down := j }).down) j'
case inr.intro
J : Type u
inst✝³ : Category J
inst✝² : IsCofilteredOrEmpty J
F : J ⥤ Type v
inst✝¹ : ∀ (j : J), Finite (F.obj j)
inst✝ : ∀ (j : J), _root_.Nonempty (F.obj j)
J' : Type (max w v u) := AsSmall J
down : J' ⥤ J := AsSmall.down
F' : J' ⥤ Type (max u v w) := down ⋙ F ⋙ uliftFunctor
this✝¹ : ∀ (i : J'), _root_.Nonempty (F'.obj i)
this✝ : ∀ (i : J'), Finite (F'.obj i)
h✝ : _root_.Nonempty J
this : IsCofiltered J
u : (j : J') → F'.obj j
hu : u ∈ Functor.sections F'
j j' : J
f : j ⟶ j'
h : F'.map { down := f } (u { down := j }) = u { down := j' }
⊢ F.map f ((fun j => (u { down := j }).down) j) = (fun j => (u { down := j }).down) j'
simp only [AsSmall.down, Functor.comp_map, uliftFunctor_map, Functor.op_map] at h
no goals
case inr.intro
J : Type u
inst✝³ : Category J
inst✝² : IsCofilteredOrEmpty J
F : J ⥤ Type v
inst✝¹ : ∀ (j : J), Finite (F.obj j)
inst✝ : ∀ (j : J), _root_.Nonempty (F.obj j)
J' : Type (max w v u) := AsSmall J
down : J' ⥤ J := AsSmall.down
F' : J' ⥤ Type (max u v w) := down ⋙ F ⋙ uliftFunctor
this✝¹ : ∀ (i : J'), _root_.Nonempty (F'.obj i)
this✝ : ∀ (i : J'), Finite (F'.obj i)
h✝ : _root_.Nonempty J
this : IsCofiltered J
u : (j : J') → F'.obj j
hu : u ∈ Functor.sections F'
j j' : J
f : j ⟶ j'
h : { down := F.map f (u { down := j }).down } = u { down := j' }
⊢ F.map f ((fun j => (u { down := j }).down) j) = (fun j => (u { down := j }).down) j'
simp_rw [← h]
no goals
case inl
J : Type u
inst✝³ : Category J
inst✝² : IsCofilteredOrEmpty J
F : J ⥤ Type v
inst✝¹ : ∀ (j : J), Finite (F.obj j)
inst✝ : ∀ (j : J), _root_.Nonempty (F.obj j)
J' : Type (max w v u) := AsSmall J
down : J' ⥤ J := AsSmall.down
F' : J' ⥤ Type (max u v w) := down ⋙ F ⋙ uliftFunctor
this✝ : ∀ (i : J'), _root_.Nonempty (F'.obj i)
this : ∀ (i : J'), Finite (F'.obj i)
h✝ : IsEmpty J
⊢ Set.Nonempty (Functor.sections F)
fconstructor <;> apply isEmptyElim