Allow (certain) maps between shapes

[TashiWalde]

There are many useful relations between shapes, such as:

1. ∆^2 is a retract of ∆^1 x ∆^1
2. ∆^1 is isomorphic to the subshape (t,s) -> s=0 of \Lambda
3. More specifically, the pair (∆^1, {1}) is isomorphic to the pair (s=0, {(1,0)}) of \Lambda

... and many more.

Currently, the only way to express these is on representables, for example as an equivalence (∆^1 -> A) = (((t,s) : \Lambda | s=0) ->A), functorial in A : U.

Of course, all of these come from actual maps on the shapes themselves, for example \ t -> (t,0) embedding ∆^1 into \Lambda. It would be very convenient if rzk would allow this.

In fact, it would probably suffice defining the primitives min, max : 2 times 2 -> 2 and 0, 1 : 1 -> 2 and then allow any function on cubes I -> J which is built from these.

(This might be related to #50)

[fizruk]

Yes, these would indeed be useful. And yes, this is related to #50.

I would also add here that one would want monotonicity axiom/property that says that for any f : 2 -> 2 and any t s : 2 we have (t ≤ s) -> (f t ≤ f s) (similar to 2mono of Weaver and Licata¹). Perhaps, there is a more general form of this for arbitrary cubes/topes. I'm also not sure yet if such an axiom should be built in when shape types are added or assumed explicitly.

One application of 2mono is to prove that coproducts of discrete types are discrete (we do not have coproducts yet, see #19), e.g. without 2mono (or a similar axiom), I think, we cannot prove that boolean type is discrete (and decidable).

Footnotes

1. Matthew Z. Weaver, Daniel R. Licata. A Constructive Model of Directed Univalence in Bicubical Sets. LICS 2020: 915-928. https://dl.acm.org/doi/pdf/10.1145/3373718.3394794 ↩