Nuprl Lemma : Kan structure on Id_A a b

We need the Kan structure on (Id_A a b).

If bx is an open box in (Id_A a b)(alpha) then it is a list of faces
<y,c,w> with w in ⌈(Id_A a b)((y:=c)(alpha))⌉

If we take x = fresh-cname(I) then ⌈¬(x ∈ I)⌉ so 
trivially,  ⌈¬(x ∈ I-[y])⌉
so we can use set-path-name(X;A;I;alpha;x;w)
to change w into an equal w' with ⌈(fst(w')) = x ∈ c-nem⌉.

We use this to 
define lift-id-face: lift-id-face(X;A;I;alpha;face)
that converts an A-face(X;(Id_A a b);I;alpha)
to an A-face(X;A;I+;iota'(I)(alpha)).

If we do this to each face in bx, we get an open box (with parameters J)
  { lift-id-faces-wf }  (proof is quite long!)
in A(iota'(I)(alpha))

Now we extend this to an open box with parameters ⌈[fresh-cname(I) / J]⌉
by adding the bottom and top faces corresponding to a(alpha) and b(alpha)
to get: cubical-id-box: cubical-id-box(X;A;a;b;I;alpha;box)
        { cubical-id-box_wf } 

We can use the Kanfiller for A
to fill it with a cube c  

Then  the pair <fresh-cname(I),c> fills the original bx in (Id_A a b)(alpha)
Kan_id_filler: Kan_id_filler(X;A;a;b).
{ Kan_id_filler_wf }

Then we have to show that this filler satisfies the uniformity condition:
  { Kan_id_filler_uniform }   (very long proof!! can it be improved?)

Putting these together we get the identity type with uniform Kan structure:
Kan-cubical-identity: Kan(Id_A a b)
{ Kan-cubical-identity_wf }.⋅

Latex:
We  need  the  Kan  structure  on  (Id\_A  a  b).

If  bx  is  an  open  box  in  (Id\_A  a  b)(alpha)  then  it  is  a  list  of  faces
<y,c,w>  with  w  in  \mkleeneopen{}(Id\_A  a  b)((y:=c)(alpha))\mkleeneclose{}

If  we  take  x  =  fresh-cname(I)  then  \mkleeneopen{}\mneg{}(x  \mmember{}  I)\mkleeneclose{}  so 
trivially,    \mkleeneopen{}\mneg{}(x  \mmember{}  I-[y])\mkleeneclose{}
so  we  can  use  set-path-name(X;A;I;alpha;x;w)
to  change  w  into  an  equal  w'  with  \mkleeneopen{}(fst(w'))  =  x\mkleeneclose{}.

We  use  this  to 
define  lift-id-face:  lift-id-face(X;A;I;alpha;face)
that  converts  an  A-face(X;(Id\_A  a  b);I;alpha)
to  an  A-face(X;A;I+;iota'(I)(alpha)).

If  we  do  this  to  each  face  in  bx,  we  get  an  open  box  (with  parameters  J)
    \{  lift-id-faces-wf  \}    (proof  is  quite  long!)
in  A(iota'(I)(alpha))

Now  we  extend  this  to  an  open  box  with  parameters  \mkleeneopen{}[fresh-cname(I)  /  J]\mkleeneclose{}
by  adding  the  bottom  and  top  faces  corresponding  to  a(alpha)  and  b(alpha)
to  get:  cubical-id-box:  cubical-id-box(X;A;a;b;I;alpha;box)
                \{  cubical-id-box\_wf  \} 

We  can  use  the  Kanfiller  for  A
to  fill  it  with  a  cube  c   

Then    the  pair  <fresh-cname(I),c>  fills  the  original  bx  in  (Id\_A  a  b)(alpha)
Kan\_id\_filler:  Kan\_id\_filler(X;A;a;b).
\{  Kan\_id\_filler\_wf  \}

Then  we  have  to  show  that  this  filler  satisfies  the  uniformity  condition:
    \{  Kan\_id\_filler\_uniform  \}      (very  long  proof!!  can  it  be  improved?)

Putting  these  together  we  get  the  identity  type  with  uniform  Kan  structure:
Kan-cubical-identity:  Kan(Id\_A  a  b)
\{  Kan-cubical-identity\_wf  \}.\mcdot{}


Date html generated: 2015_07_17-PM-06_22_08
Last ObjectModification: 2015_03_03-AM-11_34_22

Home Index