{P : Sort u} →
  {α : Type u_6} →
    {β : Type u_7} →
      {inst : Lattice α} →
        {inst_1 : Lattice β} →
          {t : LatticeHom α β} →
            {α' : Type u_6} →
              {β' : Type u_7} →
                {inst' : Lattice α'} →
                  {inst'_1 : Lattice β'} →
                    {t' : LatticeHom α' β'} →
                      α = α' → β = β' → inst ≍ inst' → inst_1 ≍ inst'_1 → t ≍ t' → LatticeHom.noConfusionType P t t'