C : Type u
inst✝³ : Category C
A B✝ X X' Y Y' Z : C
inst✝² : HasFiniteProducts C
inst✝¹ : Exponentiable A
I B : C
t : IsInitial I
inst✝ : CartesianClosed C
Z✝ : C
g h : Z✝ ⟶ I
x✝ : g ≫ IsInitial.to t B = h ≫ IsInitial.to t B
this : IsIso g
⊢ g = h
C : Type u
inst✝³ : Category C
A B✝ X X' Y Y' Z : C
inst✝² : HasFiniteProducts C
inst✝¹ : Exponentiable A
I B : C
t : IsInitial I
inst✝ : CartesianClosed C
Z✝ : C
g h : Z✝ ⟶ I
x✝ : g ≫ IsInitial.to t B = h ≫ IsInitial.to t B
⊢ g = h
haveI := strict_initial t g
C : Type u
inst✝³ : Category C
A B✝ X X' Y Y' Z : C
inst✝² : HasFiniteProducts C
inst✝¹ : Exponentiable A
I B : C
t : IsInitial I
inst✝ : CartesianClosed C
Z✝ : C
g h : Z✝ ⟶ I
x✝ : g ≫ IsInitial.to t B = h ≫ IsInitial.to t B
this✝ : IsIso g
this : IsIso h
⊢ g = h
C : Type u
inst✝³ : Category C
A B✝ X X' Y Y' Z : C
inst✝² : HasFiniteProducts C
inst✝¹ : Exponentiable A
I B : C
t : IsInitial I
inst✝ : CartesianClosed C
Z✝ : C
g h : Z✝ ⟶ I
x✝ : g ≫ IsInitial.to t B = h ≫ IsInitial.to t B
this : IsIso g
⊢ g = h
haveI := strict_initial t h
no goals
C : Type u
inst✝³ : Category C
A B✝ X X' Y Y' Z : C
inst✝² : HasFiniteProducts C
inst✝¹ : Exponentiable A
I B : C
t : IsInitial I
inst✝ : CartesianClosed C
Z✝ : C
g h : Z✝ ⟶ I
x✝ : g ≫ IsInitial.to t B = h ≫ IsInitial.to t B
this✝ : IsIso g
this : IsIso h
⊢ g = h
exact eq_of_inv_eq_inv (t.hom_ext _ _)