Nuprl Lemma : defining the Kan structure

First, we define the uniform Kan condition for 
a cubical set X.  
We really need it for the cubical dependent types,
but a cubical set with Kan structure becomes
a "constant" (i.e. independent of the context) cubical type with Kan structure
constant-Kan-type: constant-Kan-type(X)
{ constant-Kan-type_wf }.

For a given I,
we can define the family of I-faces (faces of the I-cubes)
indexed by pairs ⌈nameset(I) × ℕ2⌉
by I-face = x:nameset(I) × ℕ2 × X(I-[x])

Face <y,b,w> is face-compatible with face <z,c,u>
if (z:=c)(w) = (y:=b)(u) ∈ X(I-[y; z])  in X(I-[y; z])

A list of I-faces L is adjacent-compatible if it is
pairwise face-compatible.

Then we define open_box and the Kan filler, etc.


But, what we really need is a Kan structure on a cubical type
 Γ ⊢ A

For that, for a given  I and α in Γ(I)
we have a type A(α), and we need to define what an open box in
A(α)  is.
Here, a face will be x:nameset(I) × i:ℕ2 × A((x:=i)(α)).
We call this an A-face and define 
A-face-compatible: A-face-compatible(X;A;I;alpha;f1;f2)
A-adjacent-compatible: A-adjacent-compatible(X;A;I;alpha;L)
fills-A-faces: fills-A-faces(X;A;I;alpha;bx;L)
A-face-image: A-face-image(X;A;I;K;f;alpha;face)

The most tedious proof is to show that
the image of A-face-compatible A-faces are
A-face-compatible.  { A-face-compatible-image }.

.


.



⋅

Latex:
First,  we  define  the  uniform  Kan  condition  for 
a  cubical  set  X.   
We  really  need  it  for  the  cubical  dependent  types,
but  a  cubical  set  with  Kan  structure  becomes
a  "constant"  (i.e.  independent  of  the  context)  cubical  type  with  Kan  structure
constant-Kan-type:  constant-Kan-type(X)
\{  constant-Kan-type\_wf  \}.

For  a  given  I,
we  can  define  the  family  of  I-faces  (faces  of  the  I-cubes)
indexed  by  pairs  \mkleeneopen{}nameset(I)  \mtimes{}  \mBbbN{}2\mkleeneclose{}
by  I-face  =  x:nameset(I)  \mtimes{}  \mBbbN{}2  \mtimes{}  X(I-[x])

Face  <y,b,w>  is  face-compatible  with  face  <z,c,u>
if  (z:=c)(w)  =  (y:=b)(u)    in  X(I-[y;  z])

A  list  of  I-faces  L  is  adjacent-compatible  if  it  is
pairwise  face-compatible.

Then  we  define  open\_box  and  the  Kan  filler,  etc.


But,  what  we  really  need  is  a  Kan  structure  on  a  cubical  type
  \00CC  \mvdash{}  A

For  that,  for  a  given    I  and  \malpha{}  in  \00CC(I)
we  have  a  type  A(\malpha{}),  and  we  need  to  define  what  an  open  box  in
A(\malpha{})    is.
Here,  a  face  will  be  x:nameset(I)  \mtimes{}  i:\mBbbN{}2  \mtimes{}  A((x:=i)(\malpha{})).
We  call  this  an  A-face  and  define 
A-face-compatible:  A-face-compatible(X;A;I;alpha;f1;f2)
A-adjacent-compatible:  A-adjacent-compatible(X;A;I;alpha;L)
fills-A-faces:  fills-A-faces(X;A;I;alpha;bx;L)
A-face-image:  A-face-image(X;A;I;K;f;alpha;face)

The  most  tedious  proof  is  to  show  that
the  image  of  A-face-compatible  A-faces  are
A-face-compatible.    \{  A-face-compatible-image  \}.

.


.



\mcdot{}


Date html generated: 2015_07_17-PM-06_22_07
Last ObjectModification: 2015_03_05-PM-06_46_10

Home Index