Add combinators for Ω (addresses #43)

[ayberkt]

This PR fixes #43.

I have added subsingleton combinators as discussed in #43. Because different combinators require different assumptions, I have separated these into their own submodules. To give an example:

module Universal (fe : Fun-Ext) where

 ∀[∶]-syntax : (I : 𝓤 ̇) → (I → Ω 𝓥) → Ω (𝓤 ⊔ 𝓥)
 ∀[∶]-syntax I P = ((i : I) → P i holds) , γ
  where
   γ : is-prop ((i : I) → P i holds)
   γ = Π-is-prop fe (holds-is-prop ∘ P)


 ∀[]-syntax : {I : 𝓤 ̇} → (I → Ω 𝓥) → Ω (𝓤 ⊔ 𝓥)
 ∀[]-syntax {I = I} P = ∀[∶]-syntax I P

 infix 3 ∀[∶]-syntax
 infix 3 ∀[]-syntax
 
 syntax ∀[∶]-syntax I (λ i → e) = ∀[ i ∶ I ] e
 syntax ∀[]-syntax    (λ i → e) = ∀[ i ] e

It will usually be the case that all of these will be imported, so I also added a submodule called AllCombinators (that dependends on both propositional truncation and function extensionality) and imports all of these submodules.

[ayberkt]

@martinescardo

Just above the message that says "this branch has no conflicts with the base branch", you will see a message about the checks. When the Agda action successfully typechecks the code, that will turn green indicating that agda AllModulesIndex.lagda has succeeded.

It is a good idea to require this check to pass for all pull requests to prevent accidentally merging broken code into master. You can do this in repository settings, something involving "protected branches". You will still be able to override this requirement if you'd like but you will see some warning when doing that.

Finally, this workflow doesn't work if the author of the PR created a new module and forgot to add it to AllModulesIndex.lagda so that still has to be checked manually (but can also be automated in the future).

[martinescardo]

Thanks. All new modules should be added to index.lagda unless they are unsafe. We want unsafe modules for limited purposes only (such as showing that type-in-type leads to a contradiction, or working with Brouwerian axioms in a non-standard way by disabling the termination checker (a better way is to work with axioms, given as module or function parameters)).

[martinescardo]

Also, there are some lone modules which are deliberately not imported because they depend on the evolving cubical library, which is a moving target at the moment. I wonder how we could check them. An example is CubicalBinarySystem.lagda.

[ayberkt]

I wonder how we could check them

My Agda action actually downloads cubical every time it runs because it was needed for my development. We could use that to typecheck the modules that depend on cubical; this shouldn't be hard to do. However, it would introduce the minor complication of keeping track of the latest release version of cubical.

[martinescardo]

As I said, the cubical library is a moving target at the moment. If you look at the file mentioned above, you will see some comments explaining what to change depending one whether one uses the released version or the current version under development.
So let's leave this at that for the moment, until the next official release of the Cubical library.

[ayberkt]

If you look at the file mentioned above, you will see some comments explaining what to change depending one whether one uses the released version or the current version under development.

Ah I see what you mean now. Sure, let's leave it like this for now.