Define combinators for Ω

[ayberkt]

It is often convenient to have combinators for Ω, for instance

_∧_ : Ω 𝓤 → Ω 𝓥 → Ω (𝓤 ⊔ 𝓥)
P ∧ Q = (P holds × Q holds) , γ
 where
  γ = ×-is-prop (holds-is-prop P) (holds-is-prop Q)

agda/cubical has these defined in this module. It might be a good idea to do something similar in TypeTopology.

[ayberkt]

I defined some of these here:

https://github.com/ayberkt/TypeTopology/blob/e23b05dffe61d5aa01436a3378de0bfe63a117fb/source/Frame.lagda#L52-L65

I can send a PR creating a module with these if you are happy with the syntax.

[martinescardo]

Yes, please. Thanks.