C : Type u
inst✝¹ : Category C
inst✝ : HasWideEqualizers C
T : C
hT : ∀ (X : C), Nonempty (T ⟶ X)
endos : Type v := T ⟶ T
⊢ HasInitial C
C : Type u
inst✝¹ : Category C
inst✝ : HasWideEqualizers C
T : C
hT : ∀ (X : C), Nonempty (T ⟶ X)
⊢ HasInitial C
let endos := T ⟶ T
C : Type u
inst✝¹ : Category C
inst✝ : HasWideEqualizers C
T : C
hT : ∀ (X : C), Nonempty (T ⟶ X)
endos : Type v := T ⟶ T
i : wideEqualizer id ⟶ T := wideEqualizer.ι id
⊢ HasInitial C
C : Type u
inst✝¹ : Category C
inst✝ : HasWideEqualizers C
T : C
hT : ∀ (X : C), Nonempty (T ⟶ X)
endos : Type v := T ⟶ T
⊢ HasInitial C
let i := wideEqualizer.ι (id : endos → endos)
C : Type u
inst✝¹ : Category C
inst✝ : HasWideEqualizers C
T : C
hT : ∀ (X : C), Nonempty (T ⟶ X)
endos : Type v := T ⟶ T
i : wideEqualizer id ⟶ T := wideEqualizer.ι id
this : Nonempty endos
⊢ HasInitial C
C : Type u
inst✝¹ : Category C
inst✝ : HasWideEqualizers C
T : C
hT : ∀ (X : C), Nonempty (T ⟶ X)
endos : Type v := T ⟶ T
i : wideEqualizer id ⟶ T := wideEqualizer.ι id
⊢ HasInitial C
haveI : Nonempty endos := ⟨𝟙 _⟩
C : Type u
inst✝¹ : Category C
inst✝ : HasWideEqualizers C
T : C
hT : ∀ (X : C), Nonempty (T ⟶ X)
endos : Type v := T ⟶ T
i : wideEqualizer id ⟶ T := wideEqualizer.ι id
this✝ : Nonempty endos
this : (X : C) → Unique (wideEqualizer id ⟶ X)
⊢ HasInitial C
C : Type u
inst✝¹ : Category C
inst✝ : HasWideEqualizers C
T : C
hT : ∀ (X : C), Nonempty (T ⟶ X)
endos : Type v := T ⟶ T
i : wideEqualizer id ⟶ T := wideEqualizer.ι id
this : Nonempty endos
⊢ HasInitial C
have : ∀ X : C, Unique (wideEqualizer (id : endos → endos) ⟶ X) := by
  intro X
  refine' ⟨⟨i ≫ Classical.choice (hT X)⟩, fun a => _⟩
  let E := equalizer a (i ≫ Classical.choice (hT _))
  let e : E ⟶ wideEqualizer id := equalizer.ι _ _
  let h : T ⟶ E := Classical.choice (hT E)
  have : ((i ≫ h) ≫ e) ≫ i = i ≫ 𝟙 _ := by
    rw [Category.assoc, Category.assoc]
    apply wideEqualizer.condition (id : endos → endos) (h ≫ e ≫ i)
  rw [Category.comp_id, cancel_mono_id i] at this
  haveI : IsSplitEpi e := IsSplitEpi.mk' ⟨i ≫ h, this⟩
  rw [← cancel_epi e]
  apply equalizer.condition
no goals
C : Type u
inst✝¹ : Category C
inst✝ : HasWideEqualizers C
T : C
hT : ∀ (X : C), Nonempty (T ⟶ X)
endos : Type v := T ⟶ T
i : wideEqualizer id ⟶ T := wideEqualizer.ι id
this✝ : Nonempty endos
this : (X : C) → Unique (wideEqualizer id ⟶ X)
⊢ HasInitial C
exact hasInitial_of_unique (wideEqualizer (id : endos → endos))
C : Type u
inst✝¹ : Category C
inst✝ : HasWideEqualizers C
T : C
hT : ∀ (X : C), Nonempty (T ⟶ X)
endos : Type v := T ⟶ T
i : wideEqualizer id ⟶ T := wideEqualizer.ι id
this : Nonempty endos
X : C
⊢ Unique (wideEqualizer id ⟶ X)
C : Type u
inst✝¹ : Category C
inst✝ : HasWideEqualizers C
T : C
hT : ∀ (X : C), Nonempty (T ⟶ X)
endos : Type v := T ⟶ T
i : wideEqualizer id ⟶ T := wideEqualizer.ι id
this : Nonempty endos
⊢ (X : C) → Unique (wideEqualizer id ⟶ X)
intro X
C : Type u
inst✝¹ : Category C
inst✝ : HasWideEqualizers C
T : C
hT : ∀ (X : C), Nonempty (T ⟶ X)
endos : Type v := T ⟶ T
i : wideEqualizer id ⟶ T := wideEqualizer.ι id
this : Nonempty endos
X : C
a : wideEqualizer id ⟶ X
⊢ a = default
C : Type u
inst✝¹ : Category C
inst✝ : HasWideEqualizers C
T : C
hT : ∀ (X : C), Nonempty (T ⟶ X)
endos : Type v := T ⟶ T
i : wideEqualizer id ⟶ T := wideEqualizer.ι id
this : Nonempty endos
X : C
⊢ Unique (wideEqualizer id ⟶ X)
refine' ⟨⟨i ≫ Classical.choice (hT X)⟩, fun a => _⟩
C : Type u
inst✝¹ : Category C
inst✝ : HasWideEqualizers C
T : C
hT : ∀ (X : C), Nonempty (T ⟶ X)
endos : Type v := T ⟶ T
i : wideEqualizer id ⟶ T := wideEqualizer.ι id
this : Nonempty endos
X : C
a : wideEqualizer id ⟶ X
E : C := equalizer a (i ≫ Classical.choice (_ : Nonempty (T ⟶ X)))
⊢ a = default
C : Type u
inst✝¹ : Category C
inst✝ : HasWideEqualizers C
T : C
hT : ∀ (X : C), Nonempty (T ⟶ X)
endos : Type v := T ⟶ T
i : wideEqualizer id ⟶ T := wideEqualizer.ι id
this : Nonempty endos
X : C
a : wideEqualizer id ⟶ X
⊢ a = default
let E := equalizer a (i ≫ Classical.choice (hT _))
C : Type u
inst✝¹ : Category C
inst✝ : HasWideEqualizers C
T : C
hT : ∀ (X : C), Nonempty (T ⟶ X)
endos : Type v := T ⟶ T
i : wideEqualizer id ⟶ T := wideEqualizer.ι id
this : Nonempty endos
X : C
a : wideEqualizer id ⟶ X
E : C := equalizer a (i ≫ Classical.choice (_ : Nonempty (T ⟶ X)))
e : E ⟶ wideEqualizer id := equalizer.ι a (i ≫ Classical.choice (_ : Nonempty (T ⟶ X)))
⊢ a = default
C : Type u
inst✝¹ : Category C
inst✝ : HasWideEqualizers C
T : C
hT : ∀ (X : C), Nonempty (T ⟶ X)
endos : Type v := T ⟶ T
i : wideEqualizer id ⟶ T := wideEqualizer.ι id
this : Nonempty endos
X : C
a : wideEqualizer id ⟶ X
E : C := equalizer a (i ≫ Classical.choice (_ : Nonempty (T ⟶ X)))
⊢ a = default
let e : E ⟶ wideEqualizer id := equalizer.ι _ _
C : Type u
inst✝¹ : Category C
inst✝ : HasWideEqualizers C
T : C
hT : ∀ (X : C), Nonempty (T ⟶ X)
endos : Type v := T ⟶ T
i : wideEqualizer id ⟶ T := wideEqualizer.ι id
this : Nonempty endos
X : C
a : wideEqualizer id ⟶ X
E : C := equalizer a (i ≫ Classical.choice (_ : Nonempty (T ⟶ X)))
e : E ⟶ wideEqualizer id := equalizer.ι a (i ≫ Classical.choice (_ : Nonempty (T ⟶ X)))
h : T ⟶ E := Classical.choice (_ : Nonempty (T ⟶ E))
⊢ a = default
C : Type u
inst✝¹ : Category C
inst✝ : HasWideEqualizers C
T : C
hT : ∀ (X : C), Nonempty (T ⟶ X)
endos : Type v := T ⟶ T
i : wideEqualizer id ⟶ T := wideEqualizer.ι id
this : Nonempty endos
X : C
a : wideEqualizer id ⟶ X
E : C := equalizer a (i ≫ Classical.choice (_ : Nonempty (T ⟶ X)))
e : E ⟶ wideEqualizer id := equalizer.ι a (i ≫ Classical.choice (_ : Nonempty (T ⟶ X)))
⊢ a = default
let h : T ⟶ E := Classical.choice (hT E)
C : Type u
inst✝¹ : Category C
inst✝ : HasWideEqualizers C
T : C
hT : ∀ (X : C), Nonempty (T ⟶ X)
endos : Type v := T ⟶ T
i : wideEqualizer id ⟶ T := wideEqualizer.ι id
this✝ : Nonempty endos
X : C
a : wideEqualizer id ⟶ X
E : C := equalizer a (i ≫ Classical.choice (_ : Nonempty (T ⟶ X)))
e : E ⟶ wideEqualizer id := equalizer.ι a (i ≫ Classical.choice (_ : Nonempty (T ⟶ X)))
h : T ⟶ E := Classical.choice (_ : Nonempty (T ⟶ E))
this : ((i ≫ h) ≫ e) ≫ i = i ≫ 𝟙 T
⊢ a = default
C : Type u
inst✝¹ : Category C
inst✝ : HasWideEqualizers C
T : C
hT : ∀ (X : C), Nonempty (T ⟶ X)
endos : Type v := T ⟶ T
i : wideEqualizer id ⟶ T := wideEqualizer.ι id
this : Nonempty endos
X : C
a : wideEqualizer id ⟶ X
E : C := equalizer a (i ≫ Classical.choice (_ : Nonempty (T ⟶ X)))
e : E ⟶ wideEqualizer id := equalizer.ι a (i ≫ Classical.choice (_ : Nonempty (T ⟶ X)))
h : T ⟶ E := Classical.choice (_ : Nonempty (T ⟶ E))
⊢ a = default
have : ((i ≫ h) ≫ e) ≫ i = i ≫ 𝟙 _ := by
  rw [Category.assoc, Category.assoc]
  apply wideEqualizer.condition (id : endos → endos) (h ≫ e ≫ i)
C : Type u
inst✝¹ : Category C
inst✝ : HasWideEqualizers C
T : C
hT : ∀ (X : C), Nonempty (T ⟶ X)
endos : Type v := T ⟶ T
i : wideEqualizer id ⟶ T := wideEqualizer.ι id
this✝ : Nonempty endos
X : C
a : wideEqualizer id ⟶ X
E : C := equalizer a (i ≫ Classical.choice (_ : Nonempty (T ⟶ X)))
e : E ⟶ wideEqualizer id := equalizer.ι a (i ≫ Classical.choice (_ : Nonempty (T ⟶ X)))
h : T ⟶ E := Classical.choice (_ : Nonempty (T ⟶ E))
this : (i ≫ h) ≫ e = 𝟙 (wideEqualizer id)
⊢ a = default
C : Type u
inst✝¹ : Category C
inst✝ : HasWideEqualizers C
T : C
hT : ∀ (X : C), Nonempty (T ⟶ X)
endos : Type v := T ⟶ T
i : wideEqualizer id ⟶ T := wideEqualizer.ι id
this✝ : Nonempty endos
X : C
a : wideEqualizer id ⟶ X
E : C := equalizer a (i ≫ Classical.choice (_ : Nonempty (T ⟶ X)))
e : E ⟶ wideEqualizer id := equalizer.ι a (i ≫ Classical.choice (_ : Nonempty (T ⟶ X)))
h : T ⟶ E := Classical.choice (_ : Nonempty (T ⟶ E))
this : ((i ≫ h) ≫ e) ≫ i = i ≫ 𝟙 T
⊢ a = default
rw [Category.comp_id, cancel_mono_id i] at this
C : Type u
inst✝¹ : Category C
inst✝ : HasWideEqualizers C
T : C
hT : ∀ (X : C), Nonempty (T ⟶ X)
endos : Type v := T ⟶ T
i : wideEqualizer id ⟶ T := wideEqualizer.ι id
this✝¹ : Nonempty endos
X : C
a : wideEqualizer id ⟶ X
E : C := equalizer a (i ≫ Classical.choice (_ : Nonempty (T ⟶ X)))
e : E ⟶ wideEqualizer id := equalizer.ι a (i ≫ Classical.choice (_ : Nonempty (T ⟶ X)))
h : T ⟶ E := Classical.choice (_ : Nonempty (T ⟶ E))
this✝ : (i ≫ h) ≫ e = 𝟙 (wideEqualizer id)
this : IsSplitEpi e
⊢ a = default
C : Type u
inst✝¹ : Category C
inst✝ : HasWideEqualizers C
T : C
hT : ∀ (X : C), Nonempty (T ⟶ X)
endos : Type v := T ⟶ T
i : wideEqualizer id ⟶ T := wideEqualizer.ι id
this✝ : Nonempty endos
X : C
a : wideEqualizer id ⟶ X
E : C := equalizer a (i ≫ Classical.choice (_ : Nonempty (T ⟶ X)))
e : E ⟶ wideEqualizer id := equalizer.ι a (i ≫ Classical.choice (_ : Nonempty (T ⟶ X)))
h : T ⟶ E := Classical.choice (_ : Nonempty (T ⟶ E))
this : (i ≫ h) ≫ e = 𝟙 (wideEqualizer id)
⊢ a = default
haveI : IsSplitEpi e := IsSplitEpi.mk' ⟨i ≫ h, this⟩
C : Type u
inst✝¹ : Category C
inst✝ : HasWideEqualizers C
T : C
hT : ∀ (X : C), Nonempty (T ⟶ X)
endos : Type v := T ⟶ T
i : wideEqualizer id ⟶ T := wideEqualizer.ι id
this✝¹ : Nonempty endos
X : C
a : wideEqualizer id ⟶ X
E : C := equalizer a (i ≫ Classical.choice (_ : Nonempty (T ⟶ X)))
e : E ⟶ wideEqualizer id := equalizer.ι a (i ≫ Classical.choice (_ : Nonempty (T ⟶ X)))
h : T ⟶ E := Classical.choice (_ : Nonempty (T ⟶ E))
this✝ : (i ≫ h) ≫ e = 𝟙 (wideEqualizer id)
this : IsSplitEpi e
⊢ e ≫ a = e ≫ default
C : Type u
inst✝¹ : Category C
inst✝ : HasWideEqualizers C
T : C
hT : ∀ (X : C), Nonempty (T ⟶ X)
endos : Type v := T ⟶ T
i : wideEqualizer id ⟶ T := wideEqualizer.ι id
this✝¹ : Nonempty endos
X : C
a : wideEqualizer id ⟶ X
E : C := equalizer a (i ≫ Classical.choice (_ : Nonempty (T ⟶ X)))
e : E ⟶ wideEqualizer id := equalizer.ι a (i ≫ Classical.choice (_ : Nonempty (T ⟶ X)))
h : T ⟶ E := Classical.choice (_ : Nonempty (T ⟶ E))
this✝ : (i ≫ h) ≫ e = 𝟙 (wideEqualizer id)
this : IsSplitEpi e
⊢ a = default
rw [← cancel_epi e]
no goals
C : Type u
inst✝¹ : Category C
inst✝ : HasWideEqualizers C
T : C
hT : ∀ (X : C), Nonempty (T ⟶ X)
endos : Type v := T ⟶ T
i : wideEqualizer id ⟶ T := wideEqualizer.ι id
this✝¹ : Nonempty endos
X : C
a : wideEqualizer id ⟶ X
E : C := equalizer a (i ≫ Classical.choice (_ : Nonempty (T ⟶ X)))
e : E ⟶ wideEqualizer id := equalizer.ι a (i ≫ Classical.choice (_ : Nonempty (T ⟶ X)))
h : T ⟶ E := Classical.choice (_ : Nonempty (T ⟶ E))
this✝ : (i ≫ h) ≫ e = 𝟙 (wideEqualizer id)
this : IsSplitEpi e
⊢ e ≫ a = e ≫ default
apply equalizer.condition
C : Type u
inst✝¹ : Category C
inst✝ : HasWideEqualizers C
T : C
hT : ∀ (X : C), Nonempty (T ⟶ X)
endos : Type v := T ⟶ T
i : wideEqualizer id ⟶ T := wideEqualizer.ι id
this : Nonempty endos
X : C
a : wideEqualizer id ⟶ X
E : C := equalizer a (i ≫ Classical.choice (_ : Nonempty (T ⟶ X)))
e : E ⟶ wideEqualizer id := equalizer.ι a (i ≫ Classical.choice (_ : Nonempty (T ⟶ X)))
h : T ⟶ E := Classical.choice (_ : Nonempty (T ⟶ E))
⊢ i ≫ h ≫ e ≫ i = i ≫ 𝟙 T
C : Type u
inst✝¹ : Category C
inst✝ : HasWideEqualizers C
T : C
hT : ∀ (X : C), Nonempty (T ⟶ X)
endos : Type v := T ⟶ T
i : wideEqualizer id ⟶ T := wideEqualizer.ι id
this : Nonempty endos
X : C
a : wideEqualizer id ⟶ X
E : C := equalizer a (i ≫ Classical.choice (_ : Nonempty (T ⟶ X)))
e : E ⟶ wideEqualizer id := equalizer.ι a (i ≫ Classical.choice (_ : Nonempty (T ⟶ X)))
h : T ⟶ E := Classical.choice (_ : Nonempty (T ⟶ E))
⊢ ((i ≫ h) ≫ e) ≫ i = i ≫ 𝟙 T
rw [Category.assoc, Category.assoc]
no goals
C : Type u
inst✝¹ : Category C
inst✝ : HasWideEqualizers C
T : C
hT : ∀ (X : C), Nonempty (T ⟶ X)
endos : Type v := T ⟶ T
i : wideEqualizer id ⟶ T := wideEqualizer.ι id
this : Nonempty endos
X : C
a : wideEqualizer id ⟶ X
E : C := equalizer a (i ≫ Classical.choice (_ : Nonempty (T ⟶ X)))
e : E ⟶ wideEqualizer id := equalizer.ι a (i ≫ Classical.choice (_ : Nonempty (T ⟶ X)))
h : T ⟶ E := Classical.choice (_ : Nonempty (T ⟶ E))
⊢ i ≫ h ≫ e ≫ i = i ≫ 𝟙 T
apply wideEqualizer.condition (id : endos → endos) (h ≫ e ≫ i)