{α : Type u_6} →
  {β : Type u_7} →
    [inst : BiheytingAlgebra α] →
      [inst_1 : BiheytingAlgebra β] →
        (toFun : α → β) →
          (∀ (a b : α), toFun (a ⊔ b) = toFun a ⊔ toFun b) →
            (∀ (a b : α), toFun (a ⊓ b) = toFun a ⊓ toFun b) →
              (∀ (a b : α), toFun (a ⇨ b) = toFun a ⇨ toFun b) →
                (∀ (a b : α), toFun (a \ b) = toFun a \ toFun b) → BiheytingHom α β