case mk
C : Type u_1
inst✝ : Category C
X Y : PresheafedSpace C
β : Hom X Y
base✝ : ↑X ⟶ ↑Y
c✝ : Y.presheaf ⟶ base✝ _* X.presheaf
w : { base := base✝, c := c✝ }.base = β.base
h : HEq { base := base✝, c := c✝ }.c β.c
⊢ { base := base✝, c := c✝ } = β
C : Type u_1
inst✝ : Category C
X Y : PresheafedSpace C
α β : Hom X Y
w : α.base = β.base
h : HEq α.c β.c
⊢ α = β
cases α
case mk.mk
C : Type u_1
inst✝ : Category C
X Y : PresheafedSpace C
base✝¹ : ↑X ⟶ ↑Y
c✝¹ : Y.presheaf ⟶ base✝¹ _* X.presheaf
base✝ : ↑X ⟶ ↑Y
c✝ : Y.presheaf ⟶ base✝ _* X.presheaf
w : { base := base✝¹, c := c✝¹ }.base = { base := base✝, c := c✝ }.base
h : HEq { base := base✝¹, c := c✝¹ }.c { base := base✝, c := c✝ }.c
⊢ { base := base✝¹, c := c✝¹ } = { base := base✝, c := c✝ }
case mk
C : Type u_1
inst✝ : Category C
X Y : PresheafedSpace C
β : Hom X Y
base✝ : ↑X ⟶ ↑Y
c✝ : Y.presheaf ⟶ base✝ _* X.presheaf
w : { base := base✝, c := c✝ }.base = β.base
h : HEq { base := base✝, c := c✝ }.c β.c
⊢ { base := base✝, c := c✝ } = β
cases β
no goals
case mk.mk
C : Type u_1
inst✝ : Category C
X Y : PresheafedSpace C
base✝¹ : ↑X ⟶ ↑Y
c✝¹ : Y.presheaf ⟶ base✝¹ _* X.presheaf
base✝ : ↑X ⟶ ↑Y
c✝ : Y.presheaf ⟶ base✝ _* X.presheaf
w : { base := base✝¹, c := c✝¹ }.base = { base := base✝, c := c✝ }.base
h : HEq { base := base✝¹, c := c✝¹ }.c { base := base✝, c := c✝ }.c
⊢ { base := base✝¹, c := c✝¹ } = { base := base✝, c := c✝ }
congr