lneIt turns out a neat definition of (wild?) category(?) in #hott obtains by supposing a notion of ternary composition based on generalizing from the following equivalence in cubical type theory:
`PathP A x y ≃ (∀ w → w ≡ x → ∀ z → y ≡ z → PathP A w z)`
Only in the general (categorical) case, we formulate this as an embedding, so we have a map s.t.:
`Hom x y ↪ (∀ w → Hom w x → ∀ z → Hom y z → Hom w z)`
derived from the map, some contractibility conditions, and an interchange axiom.