Nuprl Lemma : theorems about Kan structure

The theorems about Kan structure in the Bezem, Coquand, Huber paper
are
Theorem 6.1 --that context morphisms (cubical set maps) preserve Kan structure:
  { csm-Kan-cubical-type_wf }
  { csm-Kan-id }
  { csm-Kan-comp }

Theorem 6.2 -- Pi type has Kan structure
                (that is preserved by context morphisms)
    *** not proved yet ***

Theorem 6.3 -- Sigma type has Kan structure 
                (that is preserved by context morphisms)
   { Kan-cubical-sigma_wf }
   { csm-Kan-cubical-sigma }

Theorem 7.1  -- Identity type has Kan structure
   { Kan-cubical-identity_wf }
   { csm-Kan-cubical-identity }⋅

Latex:
The  theorems  about  Kan  structure  in  the  Bezem,  Coquand,  Huber  paper
are
Theorem  6.1  --that  context  morphisms  (cubical  set  maps)  preserve  Kan  structure:
    \{  csm-Kan-cubical-type\_wf  \}
    \{  csm-Kan-id  \}
    \{  csm-Kan-comp  \}

Theorem  6.2  --  Pi  type  has  Kan  structure
                                (that  is  preserved  by  context  morphisms)
        ***  not  proved  yet  ***

Theorem  6.3  --  Sigma  type  has  Kan  structure 
                                (that  is  preserved  by  context  morphisms)
      \{  Kan-cubical-sigma\_wf  \}
      \{  csm-Kan-cubical-sigma  \}

Theorem  7.1    --  Identity  type  has  Kan  structure
      \{  Kan-cubical-identity\_wf  \}
      \{  csm-Kan-cubical-identity  \}\mcdot{}


Date html generated: 2015_07_17-PM-06_22_08
Last ObjectModification: 2015_06_29-PM-02_26_11

Home Index