MARC

 008250123s2024        us                              c    eng  d
■001000017164661
■00520250211153028
■006m          o    d                
■007cr#unu||||||||
■020    ▼a9798346759300
■035    ▼a(MiAaPQ)AAI31634570
■040    ▼aMiAaPQ▼cMiAaPQ
■0820  ▼a004
■1001  ▼aWeaver,  Matthew  Zachary.▼0(orcid)0000-0001-6959-8424
■24510▼aBicubical  Directed  Type  Theory
■260    ▼a[Sl]▼bPrinceton  University▼c2024
■260  1▼aAnn  Arbor▼bProQuest  Dissertations  &  Theses▼c2024
■300    ▼a206  p
■500    ▼aSource:  Dissertations  Abstracts  International,  Volume:  86-06,  Section:  B.
■500    ▼aAdvisor:  Licata,  Daniel  R.;Appel,  Andrew  W.
■5021  ▼aThesis  (Ph.D.)--Princeton  University,  2024.
■520    ▼aIn  homotopy  type  theory,  each  type  is  equipped  with  an  abstract  notion  of  path,  corresponding  to  the  morphisms  of  a  ∞-groupoid.  Voevodsky's  univalence  axiom  states  that  the  type  of  paths  between  types  is  equivalent  to  the  type  of  equivalences  between  types,  and  can  be  seen  as  extending  type  theory  with  a  generic  program  for  lifting  equivalences  between  types  along  any  type  family.  Defining  this  lifting  for  all  dependent  types  is  quite  subtle,  but  univalence  has  now  been  given  a  computational  interpretation  in  various  cubical  type  theories.A  natural  question  is  whether  there  are  any  directed  analogues  of  homotopy  type  theory,  where  types  are  equipped  with  a  notion  of  directed  morphism  and  correspond  to  higher  categories,  generalizing  groupoids.  In  such  a  setting,  one  possible  directed  analogue  of  univalence  would  circumscribe  a  class  of  type  constructors  that  represent  covariant  functors,  and  provide  a  means  to  automatically  lift  a  function  or  directed  morphism  along  such  a  type  constructor.  Directed  type  theory  with  directed  univalence  has  some  potential  applications  to  computer  science  that  are  not  possible  in  ordinary  homotopy  type  theory,  such  as  providing  a  convenient  language  for  coding  the  functorial  specification  of  abstract  syntax.One  approach  to  directed  type  theory,  developed  by  Riehl  and  Shulman,  is  based  on  equipping  each  type  with  both  a  notion  of  path  and  a  separate  notion  of  directed  morphism.  While  ordinary  homotopy  type  theory  has  models  in  simplicial  sets,  the  Riehl-Shulman  type  theory  is  modeled  in  bisimplicial  sets,  capturing  these  two  notions  of  path  and  directed  morphism.  While  this  suffices  for  formalizing  mathematics,  for  applications  to  computer  science  we  would  like  a  computational  interpretation  of  the  type  theory,  and  it  is  not  yet  known  whether  there  are  constructive  models  of  homotopy  type  theory  in  simplicial  sets.Thus  we  instead  consider  a  cubical  setting,  and  give  a  constructive  model  of  a  directed  type  theory  with  directed  univalence  in  bicubical  sets.  We  formalize  much  of  this  using  Agda  as  the  internal  language  of  a  topos,  following  Orton  and  Pitts.First,  building  on  the  cubical  techniques  used  to  give  computational  models  of  homotopy  type  theory,  we  show  that  there  is  a  universe  of  covariant  discrete  fibrations  with  a  partial  directed  univalence  principle  asserting  that  functions  are  a  retract  of  morphisms  in  this  universe.  To  complete  this  retraction  into  an  equivalence,  we  refine  the  model  using  Coquand,  Ruch,  and  Sattler's  work  on  constructive  sheaf  models.  We  introduce  the  cobar  modality  and  by  restricting  to  fibrant  types  that  are  also  cobar  modal,  we  are  able  to  complete  our  construction  of  directed  univalence.We  then  describe  a  generalization  of  the  fibrant  Riehl-Shulman  extension  types  defined  in  [62].  We  prove  this  in  the  setting  of  an  arbitrary  presheaf  category  with  respect  to  a  new  notion  of  fibrancy  that  is  given  by  a  generic  filling  problem.  This  abstraction  is  general  enough  to  capture  all  of  the  current  presheaf  models  of  type  theories  and  their  classifications  of  types  specified  by  filling  problems.  In  addition,  this  result  extends  the  potential  syntax  of  these  type  theories  to  be  able  to  internally  express  any  of  these  filling  problems  as  fibrant  types.  We  use  this  to  then  define  a  type  theory  in  which  the  user  can  internally  define  classifying  universes  for  any  such  filling  problem.Lastly,  we  overview  our  implementation  of  bicubical  directed  type  theory  focusing  on  a  few  interesting  design  decisions  in  regards  to  its  syntax.  As  opposed  to  exposing  the  connections  for  the  directed  interval  we  chose  to  instead  include  inequality  cofibrations  directly  in  the  syntax  and  omit  connections,  resulting  in  a  syntax  that  is  sufficiently  expressive  while  providing  substantial  benefits  computationally.
■590    ▼aSchool  code:  0181.
■650  4▼aComputer  science
■650  4▼aMathematics
■650  4▼aLogic
■653    ▼aCategory  theory
■653    ▼aHomotopy  theory
■653    ▼aHomotopy  type  theory
■653    ▼aMorphisms
■690    ▼a0984
■690    ▼a0405
■690    ▼a0395
■71020▼aPrinceton  University▼bComputer  Science.
■7730  ▼tDissertations  Abstracts  International▼g86-06B.
■790    ▼a0181
■791    ▼aPh.D.
■792    ▼a2024
■793    ▼aEnglish
■85640▼uhttp://www.riss.kr/pdu/ddodLink.do?id=T17164661▼nKERIS▼z이  자료의  원문은  한국교육학술정보원에서  제공합니다.

미리보기

내보내기

chatGPT토론

Ai 추천 관련 도서