Lean4
/-- `latToBddLat` is left adjoint to the forgetful functor, meaning it is the free
functor from `Lat` to `BddLat`. -/
def latToBddLatForgetAdjunction : latToBddLat.{u} ⊣ forget₂ BddLat Lat :=
Adjunction.mkOfHomEquiv
{ homEquiv X
_ :=
{ toFun
f :=
Lat.ofHom
{ toFun := f ∘ some ∘ some
map_sup' := fun a b => (congr_arg f <| by rfl).trans (f.hom.map_sup' _ _)
map_inf' := fun a b => (congr_arg f <| by rfl).trans (f.hom.map_inf' _ _) }
invFun f := BddLat.ofHom <| LatticeHom.withTopWithBot' f.hom
left_inv := fun f =>
BddLat.ext fun a =>
match a with
| none => f.hom.map_top'.symm
| some none => f.hom.map_bot'.symm
| some (some _) => rfl }
homEquiv_naturality_left_symm := fun _ _ =>
BddLat.ext fun a =>
match a with
| none => rfl
| some none => rfl
| some (some _) => rfl
homEquiv_naturality_right := fun _ _ => Lat.ext fun _ => rfl }
