{α : Type u_6} →
  {β : Type u_7} →
    [inst : HeytingAlgebra α] →
      [inst_1 : HeytingAlgebra β] →
        (toLatticeHom : LatticeHom α β) →
          toLatticeHom.toFun ⊥ = ⊥ →
            (∀ (a b : α), toLatticeHom.toFun (a ⇨ b) = toLatticeHom.toFun a ⇨ toLatticeHom.toFun b) → HeytingHom α β