{L : FirstOrder.Language} →
  {L' : FirstOrder.Language} →
    (toLHom : L →ᴸ L') →
      (invLHom : L' →ᴸ L) →
        invLHom.comp toLHom = FirstOrder.Language.LHom.id L →
          toLHom.comp invLHom = FirstOrder.Language.LHom.id L' → (L ≃ᴸ L')