Nuprl Lemma : The Type (Id_A a b)

To define the type (Id_A a b) we must define, for each I-cube, alpha of

the context X, the "set" (Id_A a b)(alpha).
For a new coordinate z, the members of the type
   named-path: named-path(X;A;a;b;I;alpha;z) are  z-paths from a(alpha) to b(alpha).

We tried to simply use ⌈z = fresh-cname(I) ∈ cname⌉ as the choice for coordinate z.
But, when defining the Kan structure on (Id_A a b) this did not work.
(Because then, an (y,c)-face of (Id_A a b) has coordinates
 ⌈[fresh-cname(I-[y]) / I-[y]]⌉ in A,  and that is not the same as
 ⌈[fresh-cname(I) / I]-[y]⌉ -- since fresh-cname(I-[y]) could be y  ).

So, we need to proceed as in the BCH paper with an equivalence class
of I-path: I-path(X;A;a;b;I;alpha).

The equivalence relation is 
path-eq: path-eq(X;A;I;alpha;p;q)
{ path-eq-equiv }
and the equivalence classes are the quotient type: cubical-path: cubical-path(X;A;a;b;I;alpha).

The morphisms on this type are defined by the operation: I-path-morph: I-path-morph(X;A;I;K;f;alpha;p),
and then we can define the type cubical-identity: (Id_A a b)
and prove its typing lemma { cubical-identity_wf }.

In that proof, we have to show that the morphisms are well defined on the
quotient type. So the proof is rather long and uses many lemmas
like { extend-name-morph-rename-one }
    { rename-one-extend-name-morph }
    { extend-name-morph-comp }
    { rename-one-extend-id }

The next step is to show that (Id_A a a) is inhabited by the term refl(a)
{ cubical-refl_wf }

The description of the Kan-structure is here: { Kan structure on Id_A a b }
⋅

Latex:
To  define  the  type  (Id\_A  a  b)  we  must  define,  for  each  I-cube,  alpha  of

the  context  X,  the  "set"  (Id\_A  a  b)(alpha).
For  a  new  coordinate  z,  the  members  of  the  type
      named-path:  named-path(X;A;a;b;I;alpha;z)  are    z-paths  from  a(alpha)  to  b(alpha).

We  tried  to  simply  use  \mkleeneopen{}z  =  fresh-cname(I)\mkleeneclose{}  as  the  choice  for  coordinate  z.
But,  when  defining  the  Kan  structure  on  (Id\_A  a  b)  this  did  not  work.
(Because  then,  an  (y,c)-face  of  (Id\_A  a  b)  has  coordinates
  \mkleeneopen{}[fresh-cname(I-[y])  /  I-[y]]\mkleeneclose{}  in  A,    and  that  is  not  the  same  as
  \mkleeneopen{}[fresh-cname(I)  /  I]-[y]\mkleeneclose{}  --  since  fresh-cname(I-[y])  could  be  y    ).

So,  we  need  to  proceed  as  in  the  BCH  paper  with  an  equivalence  class
of  I-path:  I-path(X;A;a;b;I;alpha).

The  equivalence  relation  is 
path-eq:  path-eq(X;A;I;alpha;p;q)
\{  path-eq-equiv  \}
and  the  equivalence  classes  are  the  quotient  type:  cubical-path:  cubical-path(X;A;a;b;I;alpha).

The  morphisms  on  this  type  are  defined  by  the  operation: 
I-path-morph:  I-path-morph(X;A;I;K;f;alpha;p),
and  then  we  can  define  the  type  cubical-identity:  (Id\_A  a  b)
and  prove  its  typing  lemma  \{  cubical-identity\_wf  \}.

In  that  proof,  we  have  to  show  that  the  morphisms  are  well  defined  on  the
quotient  type.  So  the  proof  is  rather  long  and  uses  many  lemmas
like  \{  extend-name-morph-rename-one  \}
        \{  rename-one-extend-name-morph  \}
        \{  extend-name-morph-comp  \}
        \{  rename-one-extend-id  \}

The  next  step  is  to  show  that  (Id\_A  a  a)  is  inhabited  by  the  term  refl(a)
\{  cubical-refl\_wf  \}

The  description  of  the  Kan-structure  is  here:  \{  Kan  structure  on  Id\_A  a  b  \}
\mcdot{}


Date html generated: 2015_07_17-PM-06_22_08
Last ObjectModification: 2015_03_03-PM-06_31_10

Home Index