Lean4
/-- `preordToPartOrd` is left adjoint to the forgetful functor, meaning it is the free
functor from `Preord` to `PartOrd`. -/
def preordToPartOrdForgetAdjunction : preordToPartOrd.{u} ⊣ forget₂ PartOrd Preord :=
Adjunction.mkOfHomEquiv
{ homEquiv _
_ :=
{ toFun f := Preord.ofHom ⟨f ∘ toAntisymmetrization (· ≤ ·), f.hom.mono.comp toAntisymmetrization_mono⟩
invFun
f :=
PartOrd.ofHom
⟨fun a => Quotient.liftOn' a f (fun _ _ h => (AntisymmRel.image h f.hom.mono).eq), fun a b =>
Quotient.inductionOn₂' a b fun _ _ h => f.hom.mono h⟩
left_inv _ := PartOrd.ext fun x => Quotient.inductionOn' x fun _ => rfl }
homEquiv_naturality_left_symm _ _ := PartOrd.ext fun x => Quotient.inductionOn' x fun _ => rfl }
-- The `simpNF` linter would complain as `Functor.comp_obj`, `Preord.dual_obj` both apply to LHS
-- of `preordToPartOrdCompToDualIsoToDualCompPreordToPartOrd_hom_app_coe`
