Constant square in redtt

[mortberg]

Here's a small puzzle that we will need to solve by next week: given p : Path A a a construct a square with p everywhere on the boundary.

In cubicaltt this uses lots of connections/reversals:

https://github.com/mortberg/cubicaltt/blob/master/examples/prelude.ctt#L165

We would definitely want to avoid just copying this as it will be pretty huge without native connections/reversals. Can someone come up with a direct definition like the one used for connections?

I don't think it's important what the diagonal is, but if you can get it to be p as well then you get a bonus point!

[ecavallo]

The diagonal definitely can't be p, since it will be homotopic to p · p.

[mortberg]

Hahaha, good point Evan! If you get it to be p then you get infinitely many bonus point.

[ecavallo]

Here's a (slightly more general) solution that is the size of two connections:

let connection/both
 (A : type)
 (p : dim → A) (q : [k] A [k=0 ⇒ p 1])
 : [i j] A [
   | j=0 ⇒ p i
   | i=0 ⇒ p j
   | j=1 ⇒ q i
   | i=1 ⇒ q j
   ]
 =
 λ i j →
   let face : dim → dim → A =
     λ m k →
       comp 0 m (p 1) [
       | k=0 ⇒ λ _ → p 1
       | k=1 ⇒ q
       ]
   in 
   comp 0 1 (connection/or A p i j) [
   | i=0 ⇒ λ _ → p j
   | i=1 ⇒ face j
   | j=0 ⇒ λ _ → p i
   | j=1 ⇒ face i
   ]

[mortberg]

Very nice and fast answer! Thanks Evan.

One thing that confuses me is the use of "comp"... aren't all of the compositions homogeneous?

[ecavallo]

I believe that the surface syntax comp elaborates to a com if a motive is given and an hcom otherwise.

[mortberg]

Cool!

Just a minor remark: I'm getting very owned by land 1 as they look identical in my browser's font... This makes the example quite hard to understand.

[ecavallo]

changed to an m :P

[mortberg]

Thanks! Now I see how your cube looks.

Note that the number of calls to comp in this term is 9. I wonder if this will lead to performance issues (imagine if A is a line in U...).

[ecavallo]

Here's a more direct solution which uses 7 comps:

let connection/both2
  (A : type)
  (p : dim → A) (q : [k] A [k=0 ⇒ p 1])
  : [i j] A [
    | j=0 ⇒ p i
    | i=0 ⇒ p j
    | j=1 ⇒ q i
    | i=1 ⇒ q j
    ]
  =
  λ i j →
    let pface : dim → dim → A =
      λ m k →
        comp 0 m (p 0) [
        | k=0 ⇒ λ _ → p 0
        | k=1 ⇒ p
        ]
    in
    let qface : dim → dim → A =
      λ m k → 
        comp 0 m (pface 1 k) [
        | k=0 ⇒ λ _ → p 0
        | k=1 ⇒ q
        ]
    in
    comp 0 1 (p 0) [
    | i=0 ⇒ pface j
    | i=1 ⇒ qface j
    | j=0 ⇒ pface i
    | j=1 ⇒ qface i
    ]

[ecavallo]

Here's one that uses 5:

let connection/both3
  (A : type)
  (p : dim → A) (q : [k] A [k=0 ⇒ p 1])
  : [i j] A [
    | j=0 ⇒ p i
    | i=0 ⇒ p j
    | j=1 ⇒ q i
    | i=1 ⇒ q j
    ]
  =
  λ i j →
    let pface : dim → dim → A =
      λ m k →
        comp 1 m (p k) [
        | k=0 ⇒ λ _ → p 0
        | k=1 ⇒ p
        ]
    in
    let qface : dim → dim → A =
      λ m k → 
        comp 0 m (p k) [
        | k=0 ⇒ λ _ → p 0
        | k=1 ⇒ q
        ]
    in
    comp 0 1 (p 0) [
    | i=0 ⇒ pface j
    | i=1 ⇒ qface j
    | j=0 ⇒ pface i
    | j=1 ⇒ qface i
    ]

[favonia]

I missed the party. The same trick used by the pseudo-connections still applies, and all the current pseudo-connections should be replaced by Evan's last solution immediately.

[favonia]

Actually, what I said was dumb. The current pseudo-connections are simpler and more powerful (with the correct diagonal) than the instances of Evan's final construction.