C : Type u
inst✝⁶ : Category C
inst✝⁵ : ConcreteCategory C
J : Type w
inst✝⁴ : SmallCategory J
F : J ⥤ C
inst✝³ : PreservesLimit F (forget C)
B : C
ι : Type w
inst✝² : Nonempty ι
X : ι → C
f : (j : ι) → X j ⟶ B
inst✝¹ : HasWidePullback B X f
inst✝ : PreservesLimit (wideCospan B X f) (forget C)
x y : (forget C).obj (widePullback B X f)
h : ∀ (j : ι), (forget C).map (π f j) x = (forget C).map (π f j) y
⊢ (forget C).map (base f) x = (forget C).map (base f) y
C : Type u
inst✝⁶ : Category C
inst✝⁵ : ConcreteCategory C
J : Type w
inst✝⁴ : SmallCategory J
F : J ⥤ C
inst✝³ : PreservesLimit F (forget C)
B : C
ι : Type w
inst✝² : Nonempty ι
X : ι → C
f : (j : ι) → X j ⟶ B
inst✝¹ : HasWidePullback B X f
inst✝ : PreservesLimit (wideCospan B X f) (forget C)
x y : (forget C).obj (widePullback B X f)
h : ∀ (j : ι), (forget C).map (π f j) x = (forget C).map (π f j) y
⊢ x = y
apply Concrete.widePullback_ext _ _ _ _ h
C : Type u
inst✝⁶ : Category C
inst✝⁵ : ConcreteCategory C
J : Type w
inst✝⁴ : SmallCategory J
F : J ⥤ C
inst✝³ : PreservesLimit F (forget C)
B : C
ι : Type w
inst✝² : Nonempty ι
X : ι → C
f : (j : ι) → X j ⟶ B
inst✝¹ : HasWidePullback B X f
inst✝ : PreservesLimit (wideCospan B X f) (forget C)
x y : (forget C).obj (widePullback B X f)
h : ∀ (j : ι), (forget C).map (π f j) x = (forget C).map (π f j) y
inhabited_h : Inhabited ι
⊢ (forget C).map (base f) x = (forget C).map (base f) y
C : Type u
inst✝⁶ : Category C
inst✝⁵ : ConcreteCategory C
J : Type w
inst✝⁴ : SmallCategory J
F : J ⥤ C
inst✝³ : PreservesLimit F (forget C)
B : C
ι : Type w
inst✝² : Nonempty ι
X : ι → C
f : (j : ι) → X j ⟶ B
inst✝¹ : HasWidePullback B X f
inst✝ : PreservesLimit (wideCospan B X f) (forget C)
x y : (forget C).obj (widePullback B X f)
h : ∀ (j : ι), (forget C).map (π f j) x = (forget C).map (π f j) y
⊢ (forget C).map (base f) x = (forget C).map (base f) y
inhabit ι
no goals
C : Type u
inst✝⁶ : Category C
inst✝⁵ : ConcreteCategory C
J : Type w
inst✝⁴ : SmallCategory J
F : J ⥤ C
inst✝³ : PreservesLimit F (forget C)
B : C
ι : Type w
inst✝² : Nonempty ι
X : ι → C
f : (j : ι) → X j ⟶ B
inst✝¹ : HasWidePullback B X f
inst✝ : PreservesLimit (wideCospan B X f) (forget C)
x y : (forget C).obj (widePullback B X f)
h : ∀ (j : ι), (forget C).map (π f j) x = (forget C).map (π f j) y
inhabited_h : Inhabited ι
⊢ (forget C).map (base f) x = (forget C).map (base f) y
simp only [← π_arrow f default, comp_apply, h]