case mk
C : Type u
Z : F C
n' : (Discrete ∘ NormalMonoidalObject) C
as✝ : NormalMonoidalObject C
f : { as := as✝ } ⟶ n'
⊢ ((tensorFunc C).obj Z).map f = inclusion.map f ⊗ 𝟙 Z
C : Type u
Z : F C
n n' : (Discrete ∘ NormalMonoidalObject) C
f : n ⟶ n'
⊢ ((tensorFunc C).obj Z).map f = inclusion.map f ⊗ 𝟙 Z
cases n
case mk.mk
C : Type u
Z : F C
as✝¹ as✝ : NormalMonoidalObject C
f : { as := as✝¹ } ⟶ { as := as✝ }
⊢ ((tensorFunc C).obj Z).map f = inclusion.map f ⊗ 𝟙 Z
case mk
C : Type u
Z : F C
n' : (Discrete ∘ NormalMonoidalObject) C
as✝ : NormalMonoidalObject C
f : { as := as✝ } ⟶ n'
⊢ ((tensorFunc C).obj Z).map f = inclusion.map f ⊗ 𝟙 Z
cases n'
case mk.mk.up.up
C : Type u
Z : F C
as✝¹ as✝ : NormalMonoidalObject C
h : { as := as✝¹ }.as = { as := as✝ }.as
⊢ ((tensorFunc C).obj Z).map { down := { down := h } } = inclusion.map { down := { down := h } } ⊗ 𝟙 Z
case mk.mk
C : Type u
Z : F C
as✝¹ as✝ : NormalMonoidalObject C
f : { as := as✝¹ } ⟶ { as := as✝ }
⊢ ((tensorFunc C).obj Z).map f = inclusion.map f ⊗ 𝟙 Z
rcases f with ⟨⟨h⟩⟩
case mk.mk.up.up
C : Type u
Z : F C
as✝¹ as✝ : NormalMonoidalObject C
h : as✝¹ = as✝
⊢ ((tensorFunc C).obj Z).map { down := { down := h } } = inclusion.map { down := { down := h } } ⊗ 𝟙 Z
case mk.mk.up.up
C : Type u
Z : F C
as✝¹ as✝ : NormalMonoidalObject C
h : { as := as✝¹ }.as = { as := as✝ }.as
⊢ ((tensorFunc C).obj Z).map { down := { down := h } } = inclusion.map { down := { down := h } } ⊗ 𝟙 Z
dsimp at h
case mk.mk.up.up
C : Type u
Z : F C
as✝ : NormalMonoidalObject C
⊢ ((tensorFunc C).obj Z).map { down := { down := (_ : as✝ = as✝) } } =
    inclusion.map { down := { down := (_ : as✝ = as✝) } } ⊗ 𝟙 Z
case mk.mk.up.up
C : Type u
Z : F C
as✝¹ as✝ : NormalMonoidalObject C
h : as✝¹ = as✝
⊢ ((tensorFunc C).obj Z).map { down := { down := h } } = inclusion.map { down := { down := h } } ⊗ 𝟙 Z
subst h
no goals
case mk.mk.up.up
C : Type u
Z : F C
as✝ : NormalMonoidalObject C
⊢ ((tensorFunc C).obj Z).map { down := { down := (_ : as✝ = as✝) } } =
    inclusion.map { down := { down := (_ : as✝ = as✝) } } ⊗ 𝟙 Z
simp