case mk.mk
C : Type u₁
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
F : C ⥤ D
X Y Z : C
f : Y ⟶ X
S R : Sieve X
arrows✝ : Presieve X
downward_closed✝¹ : ∀ {Y Z : C} {f : Y ⟶ X}, arrows✝ f → ∀ (g : Z ⟶ Y), arrows✝ (g ≫ f)
downward_closed✝ :
  ∀ {Y Z : C} {f : Y ⟶ X},
    { arrows := arrows✝, downward_closed := downward_closed✝¹ }.arrows f →
      ∀ (g : Z ⟶ Y), { arrows := arrows✝, downward_closed := downward_closed✝¹ }.arrows (g ≫ f)
⊢ { arrows := arrows✝, downward_closed := downward_closed✝¹ } =
    { arrows := { arrows := arrows✝, downward_closed := downward_closed✝¹ }.arrows,
      downward_closed := downward_closed✝ }
C : Type u₁
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
F : C ⥤ D
X Y Z : C
f : Y ⟶ X
S R : Sieve X
⊢ ∀ {R S : Sieve X}, R.arrows = S.arrows → R = S
rintro ⟨_, _⟩ ⟨_, _⟩ rfl
no goals
case mk.mk
C : Type u₁
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
F : C ⥤ D
X Y Z : C
f : Y ⟶ X
S R : Sieve X
arrows✝ : Presieve X
downward_closed✝¹ : ∀ {Y Z : C} {f : Y ⟶ X}, arrows✝ f → ∀ (g : Z ⟶ Y), arrows✝ (g ≫ f)
downward_closed✝ :
  ∀ {Y Z : C} {f : Y ⟶ X},
    { arrows := arrows✝, downward_closed := downward_closed✝¹ }.arrows f →
      ∀ (g : Z ⟶ Y), { arrows := arrows✝, downward_closed := downward_closed✝¹ }.arrows (g ≫ f)
⊢ { arrows := arrows✝, downward_closed := downward_closed✝¹ } =
    { arrows := { arrows := arrows✝, downward_closed := downward_closed✝¹ }.arrows,
      downward_closed := downward_closed✝ }
rfl