{L : FirstOrder.Language} →
  {M : Type w} →
    {N : Type w'} →
      [inst : L.Structure M] →
        [inst_1 : L.Structure N] →
          (toFun : M → N) →
            autoParam
                (∀ {n : ℕ} (f : L.Functions n) (x : Fin n → M),
                  toFun (FirstOrder.Language.Structure.funMap f x) = FirstOrder.Language.Structure.funMap f (toFun ∘ x))
                FirstOrder.Language.Hom.map_fun'._autoParam →
              autoParam
                  (∀ {n : ℕ} (r : L.Relations n) (x : Fin n → M),
                    FirstOrder.Language.Structure.RelMap r x → FirstOrder.Language.Structure.RelMap r (toFun ∘ x))
                  FirstOrder.Language.Hom.map_rel'._autoParam →
                L.Hom M N