∀ {X Y : FinBoolAlg} (f : X ⟶ Y),
  CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.id FinBoolAlg).map f)
      ((fun X => FinBoolAlg.Iso.mk (OrderIso.dualDual ↑X.toBoolAlg)) Y).hom =
    CategoryTheory.CategoryStruct.comp ((fun X => FinBoolAlg.Iso.mk (OrderIso.dualDual ↑X.toBoolAlg)) X).hom
      ((FinBoolAlg.dual.comp FinBoolAlg.dual).map f)