Name suggestions for lattice/category theory notions?

Stream: mathlib4

[Joël Riou]

For the development of the homotopy theory of simplicial sets, the following definition about elements in a lattice would be useful:

variable {T : Type u} (x₁ x₂ x₃ x₄ : T) [Lattice T]

structure Lattice.BicartSq where
  max_eq : x₂ ⊔ x₃ = x₄
  min_eq : x₂ ⊓ x₃ = x₁

With these assumptions, the commutative square formed by x₁, x₂, x₃, x₄ is both a pushout and a pullback square in the lattice T (considered as a category). Then, in the case T is the lattice Set X, this gives a pushout (and also a pullback) diagram in the category of types (after the application of the obvious functor Set X ⥤ Type u. Similarly, such a structure in the lattice of subpresheaves of a presheaf of sets (see docs#CategoryTheory.Subpresheaf) leads to a bicartesian square (both pushout and pullback) in the category of presheaves. This is the reason I thought naming this BicartSq, but would there be a better name?

[Joël Riou]

We would also need the following more general version in a complete lattice, and here better names are very much wanted!

variable {T : Type*} [CompleteLattice T] {ι : Type*} (X : T) (U : ι → T) (V : ι → ι → T)

structure CompleteLattice.MulticoequalizerDiagram where
  hX : X = ⨆ (i : ι), U i
  hV (i j : ι) : V i j = U i ⊓ U j

[Emily Riehl]

Coming from category theory, the name BicartSq feels very intuitive.

For the peanut gallery, @Jack McKoen gave an example of a square like this in his LeanTogether2025 talk last week (in the lattice of subpresheaves, that @Joël Riou mentioned) where the right-hand inclusion relates the n-1 skeleton to the n-skeleton of a simplicial set.

[Jack McKoen]

BicartSq seems like the most natural choice. MulticoequalizerDiagram could use some work...