case a
V : Type u
inst✝² : Category V
inst✝¹ : HasZeroMorphisms V
inst✝ : HasZeroObject V
C : CochainComplex V ℕ
X : V
f g : (single₀ V).obj X ⟶ C
h : Hom.f f 0 = Hom.f g 0
⊢ ↑(↑(fromSingle₀Equiv C X) f) = ↑(↑(fromSingle₀Equiv C X) g)
V : Type u
inst✝² : Category V
inst✝¹ : HasZeroMorphisms V
inst✝ : HasZeroObject V
C : CochainComplex V ℕ
X : V
f g : (single₀ V).obj X ⟶ C
h : Hom.f f 0 = Hom.f g 0
⊢ ↑(fromSingle₀Equiv C X) f = ↑(fromSingle₀Equiv C X) g
ext
no goals
case a
V : Type u
inst✝² : Category V
inst✝¹ : HasZeroMorphisms V
inst✝ : HasZeroObject V
C : CochainComplex V ℕ
X : V
f g : (single₀ V).obj X ⟶ C
h : Hom.f f 0 = Hom.f g 0
⊢ ↑(↑(fromSingle₀Equiv C X) f) = ↑(↑(fromSingle₀Equiv C X) g)
exact h