gistfile1.txt

Let build a Type System for mechanical verification of BROUWER’S FIXED-POINT THEOREM IN REAL-COHESIVE HOMOTOPY TYPE THEORY https://arxiv.org/pdf/1509.07584 by Shulman

Here is proposed CCHM(HoTT)/Cohesive (Im) core: Extend if needed and produce proof therm of Brower's Fixed Point Theorem in this type theory to verify mechanically. Then we will build a specialized type checker for these purposes.

type exp =
  | EPre of Z.t | EKan of Z.t | EVar of name | EHole                                 (* cosmos *)
  | EPi of exp * (name * exp) | ELam of exp * (name * exp) | EApp of exp * exp           (* pi *)
  | ESig of exp * (name * exp) | EPair of tag * exp * exp | EFst of exp | ESnd of exp (* sigma *)
  | EId of exp | ERef of exp | EJ of exp | EField of exp * string           (* strict equality *)
  | EPathP of exp | EPLam of exp | EAppFormula of exp * exp                   (* path equality *)
  | EI | EDir of dir | EAnd of exp * exp | EOr of exp * exp | ENeg of exp     (* CCHM interval *)
  | ETransp of exp * exp | EHComp of exp * exp * exp * exp                   (* Kan operations *)
  | EPartial of exp | EPartialP of exp * exp | ESystem of exp System.t    (* partial functions *)
  | ESub of exp * exp * exp | EInc of exp * exp | EOuc of exp              (* cubical subtypes *)
  | EGlue of exp | EGlueElem of exp * exp * exp | EUnglue of exp                    (* glueing *)
  | EEmpty | EIndEmpty of exp                                                             (* 𝟎 *)
  | EUnit | EStar | EIndUnit of exp                                                       (* 𝟏 *)
  | EBool | EFalse | ETrue | EIndBool of exp                                              (* 𝟐 *)
  | EW of exp * (name * exp) | ESup of exp * exp | EIndW of exp * exp * exp               (* W *)
  | EIm of exp | EInf of exp | EIndIm of exp * exp | EJoin of exp    (* Infinitesimal Modality *)