∀ (X : Lat) (x : BddLat) (f : latToBddLat.obj X ⟶ x) (a b : ↑X),
  (CategoryTheory.ConcreteCategory.hom f) ((some ∘ some) (a ⊓ b)) =
    (⇑(CategoryTheory.ConcreteCategory.hom f) ∘ some ∘ some) a ⊓
      (⇑(CategoryTheory.ConcreteCategory.hom f) ∘ some ∘ some) b