WIP Diaconescu's theorem

[clayrat]

Currently I'm stuck defining the P family in suspension-lemma for the double merid case :(

[jonsterling]

@clayrat Cool! I'll try and have a look this weekend.

[clayrat]

I've tried plugging that case with a filler like this:

def helper (A : type) (A/prop : is-prop A) (a : A) (i j : 𝕀) : type =
   let A→U = ua A unit (prop/unit A A/prop a) in
   let U→A = symm^1 type A→U in
   comp 0 i (U→A j) [
   | j=0 → U→A
   | j=1 → A→U
   ]

but that spits up an mismatched top frames error.

[jonsterling]

@clayrat I think I have some idea of what is going on :smile:

[clayrat]

@jonsterling Does this have something to do with the path/identity distinction, or is it something more prosaic? :)

[jonsterling]

@clayrat My guess is that it has to do with that issue I mentioned on IRC where you need some elim form to have the exact right boundary. Sorry I didn't have a chance to look at this on the weekend: there were some things happening in Pittsburgh that demanded my attention.

[clayrat]

I've tried adding the motive, but now the hole became something like a j/k-square, where the j side involves a function on k, and vice versa the k side depends on j, and I'm no longer sure this is making sense :D

[clayrat]

Hm, it looks like that hole should be pluggable by connection/both^1 type (uA a) (Au a) k j, but it gives me a "global variable name mismatch" ¯_(ツ)_/¯

EDIT: Nevermind, it involves a square with as on horizontals and bs on verticals, can be seen more easily with the code at https://github.com/RedPRL/redtt/pull/461

[clayrat]

Ok I think I've narrowed down the construction of P to this helper :

  def help (A : type) 
    (abx : 𝕀 → A) 
    (aby : [k] A [k=0 → abx 0 | k=1 → abx 1]) 
    (bax : [k] A [k=0 → abx 1 | k=1 → abx 0]) 
    (bay : [k] A [k=0 → abx 1 | k=1 → abx 0]) 
    (abxy : path (𝕀 → A) abx aby)
    (baxy : path (𝕀 → A) bax bay)
  : [i j] A [
    | i=0 → aby j 
    | i=1 → bay j 
    | j=0 → abx i 
    | j=1 → bax i
    ]
  = ?help

then merid-hole can be plugged with help^1 type (uA a) (uA b) (Au a) (Au b) (λ k → uA (A/prop a b k)) (λ k → Au (A/prop a b k)) i j but I can't figure out how to construct the helper square :(

[ecavallo]

In the place you are using helper, are the paths abxy and baxy actually of type path (path A (abx 0) (abx 1)) abx aby and path (path A (abx 1) (abx 0)) bax bay respectively? The way they are stated (as paths in 𝕀 → A), they won't be useful in helper, as 𝕀 → A is already contractible.

[ecavallo]

If they do have those stronger types, then this should work:

def help (A : type) 
  (abx : 𝕀 → A) 
  (aby : path A (abx 0) (abx 1))
  (bax : path A (abx 1) (abx 0))
  (bay : path A (abx 1) (abx 0))
  (abxy : path (path A (abx 0) (abx 1)) abx aby)
  (baxy : path (path A (abx 1) (abx 0)) bax bay)
  : [i j] A [
    | i=0 → aby j 
    | i=1 → bay j 
    | j=0 → abx i 
    | j=1 → bax i
    ]
  =
  λ i j →
  comp 0 1 (connection/both A abx bax i j) [
  | i=0 k → abxy k j
  | i=1 k → baxy k j
  | ∂[j] → refl
  ]

Otherwise, I think helper is not definable.

[clayrat]

@ecavallo yeah, those are basically paths^1 between A→unit and unit→A defined by univalence

[clayrat]

@ecavallo Oh wow, I have been using that exact term and didn't realize the path types are wrong!!! Thanks!