redtt icon indicating copy to clipboard operation
redtt copied to clipboard
verified publisher icon RedPRL

WIP Diaconescu's theorem

Open clayrat opened this issue 7 years ago β€’ 12 comments

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

clayrat avatar Oct 31 '18 23:10 clayrat

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

jonsterling avatar Nov 02 '18 12:11 jonsterling

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.

clayrat avatar Nov 02 '18 12:11 clayrat

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

jonsterling avatar Nov 02 '18 15:11 jonsterling

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

clayrat avatar Nov 05 '18 13:11 clayrat

@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.

jonsterling avatar Nov 05 '18 13:11 jonsterling

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 avatar Nov 05 '18 17:11 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 avatar Nov 05 '18 23:11 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 :(

clayrat avatar Nov 06 '18 15:11 clayrat

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 avatar Nov 06 '18 16:11 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.

ecavallo avatar Nov 06 '18 16:11 ecavallo

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

clayrat avatar Nov 06 '18 16:11 clayrat

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

clayrat avatar Nov 06 '18 16:11 clayrat