호모토피형 이론

수학적 논리학 및 컴퓨터학에서 호모토피형 이론(HoTT /h/t/)은 (추상) 호모토피 이론의 직관이 적용되는 개체로서의 유형에 대한 해석에 기초하여 직관형 이론의 다양한 발전 라인을 말한다.null

여기에는 이러한 유형의 이론에 대한 동음이의학 및 상위 범주의 모델의 구축, 추상적인 동음이의학 이론과 상위 범주 이론에 대한 논리(또는 내부 언어)로서의 유형 이론의 사용, 유형-이론 기반 내에서 수학의 개발(이전에 존재하는 수학 모두 포함)이 포함된다.동음이의어 유형이 가능하게 하는 역학과 새로운 수학; 그리고 컴퓨터 교정 보조원들에게 이것들 각각을 공식화.null

호모토피형 이론이라고 하는 작품과 단발성 기반 프로젝트라고 하는 작품 사이에는 큰 중복이 있다.둘 다 정확하게 기술되어 있지 않으며, 용어가 서로 교환하여 사용되기도 하지만, 사용의 선택은 또한 때로는 관점과 강조의 차이와 일치하기도 한다.^[1]이와 같이, 이 기사는 그 분야의 모든 연구자들의 견해를 동등하게 표현하지 않을 수도 있다.어떤 장이 급속도로 유동할 때 이러한 종류의 변동성은 피할 수 없다.null

역사

선사시대: 조로이드 모형

한때 자신의 정체성을 가진 강렬형 이론의 활자를 집단형(groupoids)으로 볼 수 있다는 생각은 수학적인 민속학이었다.그것은 마틴 호프만과 토마스 스트레이셔의 1998년 논문에서 "유형 이론의 집단적 해석"이라고 불리는 의미론적으로 처음으로 정밀하게 만들어졌는데, 이 논문은 강도적 유형 이론이 집단형 이론의 범주에 모델을 가지고 있다는 것을 보여주었다.^[2]이것이 비록 "1차원(동형학적으로 0차원인 집합의 범주의 전통적인 모델)에 불과하지만, 형식 이론의 진정한 최초의 "동형학" 모델이었다.null

그들의 논문은 또한 호모토피형 이론의 몇 가지 후발전을 예시했다.예를 들어, 그들은 그룹형 모델이 그들이 "단일우주 확장성"이라고 부르는 규칙을 충족시킨다고 언급했는데, 이것은 다름아닌 블라디미르 보에보스키가 10년 후에 제안한 단일성 공리의 1유형에 대한 제한이다.(단, "평등"이라는 일관된 개념이 필요하지 않기 때문에, 1-유형에 대한 공리는 특히 공식화하기가 더 간단하다.그들은 또한 "균등성을 가진 범주"를 정의했고, 고차원 그룹오이드를 사용하는 모델에서 그러한 범주에 대해 "평등성은 평등"을 가질 것이라고 추측했다; 이것은 베네딕트 아렌스, 크리즈토프 카풀킨, 그리고 마이클 슐만에 의해 나중에 증명되었다.^[3]null

초기 역사: 모델 카테고리 및 상위 그룹오이드

강화형 이론의 첫 번째 고차원 모델은 스티브 어워디와 그의 제자인 마이클 워렌에 의해 2005년에 퀼렌 모델 카테고리를 사용하여 만들어졌다.이러한 결과는 워렌이 '강화형 이론의 호모토피 모델'이라는 제목의 강연을 한 FMCS 2006^[4] 회의에서 처음으로 공개되었는데, 이 강연은 그의 논문 발표자(현재의 논문 위원회는 아워디, 니콜라 감비노, 알렉스 심슨)이기도 했다.Warren의 논문 개요에 요약이 포함되어 있다.^[5]null

2006년^[6] 웁살라 대학교에서 열린 ID 타입에 대한 후속 워크숍에서는 강도 타입 이론과 인자화 시스템 사이의 관계에 대한 두 가지 논의가 있었다. 하나는 리처드 가너, 다른 하나는 "유형 이론을 위한 팩토리화 시스템"^[7]이고 다른 하나는 마이클 워렌, "모델 카테고리 및 강도 ID 타입"이다.관련 아이디어는 스티브 어워디(Steve Awodey)와 토마스 스트레이셔(Thomas Streicher)의 '고차원 카테고리의 유형론'과 '아이덴티티 유형 대 약한 오메가-그룹: 일부 아이디어, 일부 문제'가 회담장에서 논의됐다.같은 컨퍼런스에서 벤노 판 덴 버그는 "약약한 오메가 범주로서의 유형"이라는 주제로 강연을 했는데, 거기서 그는 나중에 리처드 가너와 공동 논문의 주제가 된 아이디어를 개략적으로 설명했다.null

고차원 모델의 초기구축은 모두 종속형 이론의 전형적 일관성의 문제를 다루어야 했고, 다양한 해결책이 개발되었다.그 중 하나는 2009년 보에보스키에 의해, 또 다른 하나는 2010년 판 덴 버그와 가너에 의해 주어졌다.^[8]Voevodsky의 건설에 기반한 일반적인 해결책은 결국 2014년 Lumsdaine과 Warren에 의해 주어졌다.^[9]null

2007년^[10] PSSL86에서 아워디는 '호모토피형 이론'(Awody가^[11] 만든 그 용어의 첫 번째 공용어였다.)이라는 제목으로 강연을 했다.아워디와 워렌은 2007년^[12] 아르시브 프리프린트 서버에 게재돼 2009년 출간된 '아이덴티티 유형의 호모토피 이론 모델' 논문에서 이들의 결과를 요약했고, 2008년 워런의 논문 '건설형 이론의 호모토피 이론 측면'에 더 자세한 버전이 등장했다.null

그와 거의 동시에 블라디미르 보에보드스키는 수학의 실질적인 형식화를 위한 언어의 탐색이라는 맥락에서 활자 이론을 독자적으로 조사하고 있었다.2006년 9월에 그는 "호모토피 람다 미적분에 관한 매우 짧은 노트"^[13]라는 메일링 리스트에 글을 올렸는데, 이 메일 리스트는 의존적인 제품, 합계, 우주가 있는 형식 이론의 개요와 Kan simplicical sets에서 이러한 형식 이론의 모델을 스케치한 것이다.'호모토피 λ-미적분은 가설적(현재)형 체계'라는 말로 시작돼 "현재 내가 위에서 말한 것 중 상당 부분이 추측 수준에 있다"는 말로 끝을 맺었다.호모토피 범주에서 TS 모델의 정의조차 '비경쟁적'으로 2009년까지 해결되지 않았던 복잡한 일관성 문제를 언급하고 있다.이 노트에는 "평등 유형"에 대한 통사적 정의가 포함되었는데, 이 정의는 경로 공간에 의해 모델에서 해석된다고 주장되었지만, ID 유형에 대한 Per Martin-Löf의 규칙은 고려하지 않았다.그것은 또한 크기 외에도 호모토피 차원에 의해 우주를 층화시켰는데, 이것은 나중에 대부분 폐기된 아이디어였다.null

통사적 측면에서는 2006년 벤노 판 덴 버그가 마이클 바타닌의 "광학, 대수학" 감각에서 강도형 이론의 한 유형의 정체성 유형의 탑은 Ω 범주의 구조, 그리고 실제로 Ω-그룹형 구조를 가져야 한다고 추측했다.이것은 나중에 판 덴 버그와 가너에 의해 "유형은 약한 오메가-그룹" (2008년 발간) 논문에서,^[14] 그리고 피터 럼스데인은 "강화유형 이론에서 나온 약 Ω-범주" (2009년 발간) 논문에서, 그리고 2010년 박사 논문 "유형 이론에서 나온 상위 범주"^[15]의 일부로 독립적으로 증명되었다.null

단발성 공리, 합성 호모토피 이론 및 상위 귀납형

단발성 진동의 개념은 2006년 초 Voevodsky에 의해 도입되었다.^[16]그러나 텅 빈 맥락에서 신분 유형이 반사성만을 포함할 수 있는 성질에 대한 마틴 뢰프형 이론의 모든 제시가 주장되었기 때문에, 보에보드스키는 이러한 신분 유형이 단생적인 우주와 결합하여 사용될 수 있다는 것을 2009년까지 인식하지 못했다.특히 기존의 마틴 뢰프식 이론에 공리를 가미하면 단순히 단일성을 도입할 수 있다는 생각은 2009년에야 등장했다.null

또한 2009년 보에보드스키는 칸 콤플렉스에서의 유형론 모델의 세부사항을 더 많이 도출해냈고, 보편적인 칸진동의 존재가 유형론의 범주형 모델에 대한 일관성 문제를 해결하는 데 이용될 수 있다고 관찰했다.그는 또한 A. K. Bousfield의 아이디어를 사용하여 이 보편적인 진동이 단발적이라는 것을 증명했다: 섬유들 사이의 쌍방향 동종 동종 균등성의 관련 진동은 기지의 경로 공간 진동과 동등하다.null

단일성을 공리로 공식화하기 위해 Voevodsky는 "f는 동등함"이라는 문구를 나타내는 유형이 (기능 확장성의 가정 하에서)-1)-트런(즉, 존재하는 경우 계약 가능)이라는 중요한 속성을 갖는 "평등성"을 구문론적으로 정의하는 방법을 찾았다.이것은 호프만과 스트레이셔의 "단일적인 확장성"을 더 높은 차원으로 일반화하면서 그가 단일성에 대한 통사적 진술을 할 수 있게 했다.그는 또한 증명 보조자 Coq에서 상당한 양의 "합성 호모토피 이론"^[17]을 개발하기 시작하기 위해 동등성과 계약성에 대한 이러한 정의를 사용할 수 있었다; 이것은 나중에 "창업자"라고 불리는 도서관의 기초를 형성했다.null

다양한 실의 통일은 2010년 2월 카네기 멜론 대학교에서 비공식적인 만남으로 시작되었는데, 그곳에서 보에보드스키는 아워디, 워렌, 럼스다인, 로버트 하퍼, 댄 리카타, 마이클 슐먼 등 여러 그룹에 간 콤플렉스의 모델과 그의 코크 코드를 제시했다.이 회의는 모든 호모토피 동등성이 동등성을 (보보보드스키의 좋은 일관성 있는 의미에 있어서) 동등성을 개선한다는 범주론에서 부호화 동등성으로의 개념에 근거하여 동등하다는 증거(워렌, 럼스다인, 리카타, 슐만)의 개요를 도출했다.곧이어 보보드스키는 단발성 공리가 함수 확장성을 내포하고 있음을 증명했다.null

다음 중추적 행사는 2011년 3월 스티브 아워디, 리처드 가너, 페르 마틴 뢰프, 블라디미르 보보드스키가 주최한 오버울프치 수학연구소 미니워크숍으로, '건설형 이론의 호모토피 해석'^[18]이라는 제목이 붙었다.올해 워크숍에 대한 끓여라 튜토리얼의 일환으로, Andrej 바우어가 작은 끓여라 library[19]보예 보츠키의 생각을 바탕(지만 그의 코드를 이용하고 있지 않);"HoTT" 끓여라 library[20]의 첫 버전의 이 되었고 그 커널은 latter[21]의 마이클 슐먼"Andrej 바우어의 파일을 기준 개발, 재치 있다고 지적하고(첫번째 참가를 썼다.h 많은 생각"Vladimir Voevodsky 파일에서 가져옴").올버울프차치 모임에서 가장 중요한 것 중 하나는 럼스다인, 슐만, 바우어, 워렌 때문에 더 높은 귀납형식의 기본이념이었다.참가자들은 또한는지 등의 일가 공리, 그 일가 공리(이후 긍정적으로 슐먼에 의한 답변을)비표준 모델들을 가지고 있고, 어떻게(4)simplicial를(여전히 op 교회 법에 합치함(비록 몇가지 특별한 일들이 해결되어서 여전히 열려 진 positively[22][23])을 만족시킬 만큼 중요한 공개적인 문제의 목록을 공식화했습니다.M에 앙LTT, 비록 보에보스키의 호모토피 타입 시스템(HTS)에서 할 수 있지만, 두 가지 동일 유형을 가진 타입 이론이다.null

오베르울프치 워크숍 직후 호모토피형 이론 웹사이트와 블로그가^[24] 개설되었고, 그 이름으로 주제가 대중화되기 시작했다.이 기간 동안의 중요한 진보의 일부는 블로그의 역사에서 얻을 수 있다.^[25]null

단발적 기초

'단일적 기초'라는 말은 호모토피형 이론과 밀접하게 관련되기로 모두가 동의하지만, 모두가 같은 방식으로 사용하는 것은 아니다.원래 블라디미르 보보드스키가 단발성 공리를 만족하는 형식 이론에 근거하여 기본적인 사물이 호모토피 유형인 수학의 기초체계에 대한 그의 비전을 언급하기 위해 사용하였으며, 컴퓨터 증명 보조자로 공식화되었다.^[26]null

으로서 보예 보츠키의 작품 다른 연구원들 동위 유형론에 대해 함께 일하는 사회와 통합이 되었습니다,"일가 재단"가끔 서로 대체 가능한 것과 다른"호모토피 유형론"[27]번만 가지고는 그 사용에 근본적 시스템으로(으로 사용되었어를 제외한, 예를 들어,model-categorical 의미 또는 계산의 연구.알 m에타테오리의^[28]예를 들어, IAS 특별연도의 주제는 공식적으로 "단일적인 기초"로 지정되었다. 비록 많은 작업이 재단 외에도 의미론과 메타테리학에 집중되어 있었지만 말이다.IAS 프로그램 참여자들이 작성한 책의 제목은 "호모토피 유형 이론:수학의 단발적인 기초"; 비록 이것은 어느 하나의 용법을 언급할 수 있지만, 이 책은 HoTT를 수학적 기초로서만 논하기 때문이다.^[27]null

수학의 독창적인 기초에 관한 특별한 해

2012-13년 고등연구원의 연구자들은 "수학의 독창적인 기초에 관한 특별한 해"를 개최했다.^[29]이 특별한 해에는 위상, 컴퓨터 과학, 범주 이론, 수학 논리학 분야의 연구자들이 모였다.이 프로그램은 스티브 어워디, 티에리 코콴드, 블라디미르 보보드스키가 기획했다.null

프로그램 동안 참가자들 중 한 명이었던 Peter Aczel은 정해진 이론을 수행하는 일반 수학자들과 유사한 스타일로 형식 이론을 비공식적이지만 엄격하게 수행하는 방법을 연구하는 작업 그룹을 시작했다.초기 실험 후, 이것이 가능할 뿐만 아니라 매우 유익하다는 것이 분명해졌고, 책(일명 HoTT Book)^[27][30]은 쓸 수 있고 또 써야 한다.그 후 많은 다른 참여자들이 기술 지원, 글쓰기, 교정 읽기, 아이디어 제공에 동참했다.수학 교과서는 이례적으로 공동 개발되어 GitHub에 공개되었으며, 책을 포크링할 수 있는 크리에이티브 커먼즈 라이센스에 따라 공개되며, 인쇄물 및 다운로드도 무료로 구입할 수 있다.^[31][32][33]null

보다 일반적으로, 이 특별한 해는 전체 주제를 발전시키는 촉매제였다; HoTT 책은 비록 가장 눈에 띄는 결과이긴 하지만 단 하나였다.null

특별연도의 공식참가자

ACM Computing Reviews는 이 책을 "컴퓨팅의 수법" 범주에 있는 주목할 만한 2013년 간행물로 열거했다.^[34]null

주요개념

강렬형 이론	호모토피 이론
$A{\displaystyle }$ 유형 ${\displaystyle A}$	$공백{\displaystyle }$ A ${\displaystyle A}$
$용어$는 a$([\displaystyle a}$	$[\displaystyle a}$을(를) 가리킨다.
${\displaystyle a:A}$	$A에서 A를 표시하십시오.$
종속형 ${\displaystyle x:A\ \vdash \ B(x)\ }$	진동 $B\to A}$
신분 유형 ${\displaystyle \mathrm {Id} _{A}(a,b)}$	경로 공간
${\displaystyle p:\mathrm {Id} _{A}(a,b)}$	경로 $p:a\to b}$
${\displaystyle \alpha :\mathrm {Id} _{\mathrm {Id} _{A}(a,b)}(p,q)}$	호모토피 ${\displaystyle \alpha :p\오른쪽 화살표 q}$

"유형 제안"

HoTT는 형식 이론의 "유형으로서의 제안" 해석의 변형된 버전을 사용하며, 형식은 또한 명제를 나타낼 수 있고 용어는 증거를 나타낼 수 있다.그러나, HoTT에서는 표준 "유형 제안"과는 달리, 대략적으로 말해서, 명제적 평등에 이르기까지 하나의 용어를 가진 '미어 명제'에 의해 특별한 역할을 수행한다.이것들은 증거와 관련이 없다는 점에서 일반적인 유형이라기 보다는 전통적인 논리적 명제에 가깝다.null

평등

호모토피형 이론의 기본 개념은 경로다.HoTT에서 유형 $a{\displaystyle }$= ${\displaystyle b}$ ${\$$displaystyle a}$에서 $포인트{\displaystyle }$ b ${\displaystyle b}$까지 모든 경로의 유형$$$($$따라서$$,$ 포인트 $}$이(가) 포인트 $b{\displaystyle }$ ${\$$displaystyle$b}과(따라서, 포인트 a)가 포인트$$ b ${\displaystystyle$ b$}$에서 포인트까지의$$ 경로와 동일하다는 증거가 된다$$.${\displaystyle b}$ ${\displaystyle b$$}$ .)$$ $어떤{\displaystyle }$ 점에 $대해서$도$,$${\displaystyle a}$ =$${\$displaystyle a}$ 유형의 경로는 평등의 반사적 속성에 해당하는 것이 있다$.$$a{\displaystyle }$= ${\displaystyle b}$ ${\displaystyle a=b}$ 유형의 경로는 반전될 수 있으며$$$,$ 평등의 대칭 속성에 해당하는 ${\displaystyle b}$= ${\displaystyle b=a}$ 유형의 경로를 형성한다.$a{\displaystyle }$ =${\displaystyle b}$ = b ${\displaystyle a=$b$$} $.$ ${\displaystyle b}$ = c {\$displaystyle b=c$} 유형의 두 경로를 $연결$하면${\displaystyle }$a = ${\displaystyle c}${\$displaystyle a=c$ 이는 평등의 타동적 속성에 해당한다.null

Most importantly, given a path ${\displaystyle p:a=b}$, and a proof of some property ${\displaystyle P(a)}$, the proof can be "transported" along the path ${\displaystyle p}$ to yield a proof of the property ${\displaystyle P(b)}$. (Equivalently stated, an object of type ${\displaysty$$le$P($a)}$을(를${\displaystyle )}$ 유형 P$($ ) {\$displaystyle$ P(b$)}$의 개체로 변환할$$ 수 있다.)$$이것은 평등의 대체 속성에 해당한다.여기서 HoTT와 고전 수학의 중요한 차이가 들어온다.고전 수학에서$,$ $일단{\displaystyle }$ 두 값 a와$$$b$의 동일성이 확립되면$$, $그것들{\displaystyle }$ 사이의 어떠한 구별도 고려하지 않고, 그 후에 ${\디스플레이$ 스타일$$ a$}$과 $b$ ${\표시$ 스타일 $b}$을 서로 교환하여 사용할 수 있다.그러나 호모토피형 이론에서는 $a{\displaystyle }$= ${\displaystyle b}$ ${\displaystyle a=b}$이(가) 여러 개의 다른 경로가 있을 수 있으며$,$ 두 개의 다른 경로를 따라 물체를 운반하는 것은 두 가지 다른 결과를 산출할 수 있다.따라서 호모토피형 이론에서는 대체 특성을 적용할 때 어떤 경로를 사용하고 있는지를 명시할 필요가 있다.null

일반적으로, "제안"은 여러 가지 다른 증거를 가질 수 있다. (예를 들어, 모든 자연수의 유형은, 명제로 간주될 때, 모든 자연수를 증거로서 가지고 있다.제안이 하나의 $증거$만 가지고 있더라도 경로 $a{\displaystyle }$= ${\displaystyle a}$ = ${\displaystyle a=a}$의 공간은 어떤 면에서 비교가 되지 않을 수 있다$$$.$"미어 명제"는 비어 있거나 사소한 경로 공간이 있는 하나의 점만 포함하는 모든 유형이다.null

${\displaystyle \mathrm{사람들}}$은 $I{\displaystyle }$ ${\displaystyle d_{}}$ A${\displaystyle {}_{}}$( ,${\displaystyle b}$) ${\displaystyle Id_{A}(a,b$에 $대해{\displaystyle }$a = b$${\$displaystyle$ a$,b}$을(를) 쓰기 때문에${\displaystyle ,}$ $a{\displaystyle }$, ${\displaystyle b}${\$displaystyle a,b}$의 $형식{\displaystyle }$ A ${\displaystystyle A}$을(를)가 암묵적으로$$ 남겨둔다는 점에 유의하십시오.$i{\displaystyle }$ ${\displaystyle {}_{}}$ ${\displaystyle A_{}}$: ${\displaystyle A}$→ A ${\displaystyle id_{$$A{\displaystyle }$$:A\to A$ A ${\displaystyle A}$에서 ID 함수를 나타냄$.$

유형균등성

일부 우주 $U{\displaystyle }$ ${\displaystyle U}$에 속하는$$ 두 가지 $유형{\displaystyle }$ A ${\$displaystyle $A}$ 및 $B$ ${\displaystyle B}$은(는) 동등성이 존재하는 경우 동등한 것으로 정의된다.등가성은 함수다.

${\displaystyle f:A\to B}$

적절하게 선택된 $g{\displaystyle }$ ${\displaystyle g}$ 및$$ $h{\displaystyle }$ ${\displaystyle h}$의 경우, 왼쪽 역과 오른쪽 역이 모두 존재한다는 의미에서 다음과 같은 유형이 모두 존재한다$.$

${\displaystyle Id_{B\오른쪽 화살표 B}(f\circule g,id_{B}),}$

${\displaystyle Id_{A\오른쪽 화살표 A}(h\circule f,id_{A}).}$

즉

${\displaystyle f\circle g=_{B\오른쪽 화살표 B}id_{B}}}$

${\displaystyle h\circ f=_{A\오른쪽 화살표 A}id_{A}.}$

이는 동일 유형을 사용하여 "${\displaystyle }$ ${\displaystyle f}$에 왼쪽 역과 오른쪽 역이 모두$$ 있다"는 일반적인 개념을 나타낸다.위의 역직성 조건은 기능 $유형{\displaystyle }$ A${\displaystyle }$→ ${\displaystyle A}$ → A $[\displaystyle$ A$\rightarrow A}$ $및$ ${\displaystyle B}$→ B$[\displaystyle B\rightarrow B}$에 있는 동일성 유형이라는 점에 유의하십시오$.$ 일반적으로 기능 확장성 공리를 가정하며, 이는 동등성을 사용하여 역직성을 나타내는 다음 유형과 동일함을 보장한다.n 도메인 및 코드체인 $A{\displaystyle }$ ${\displaystyle A}$ $및$ B ${\displaystyle B$

${\displaystyle \Pi _{y:B}.\ Id_{B}(f\circ g)(y),id_{B}(y),}$

${\displaystyle \Pi _{x:A}.\ Id_{A}((h\circ f)(x),id_{A}(x)).}$

${\displaystyle 예}$: ${\displaystyle \mathrm{모든}}$ $x{\displaystyle }$: A ${\displaystyle x:A}$ $및$ y${\displaystyle }$: B ${\displaystyle y:$$B}$,

$(\displaystyle f(g(y)))=_{B}y,}$

$(\displaystyle h(f(x)))=_{A}x.}$

타입의 함수

$A\to B}$

그것들이 동등하다는 증거와 함께 에 의해 증명된다.

${\displaystyle A}$ ${\displaystyle \simeq }$ B ${\displaystyle A\simeq$ B$\}.$

단발성 공리

위와 같은 동등성 함수를 정의하면 동등성으로의 경로를 전환하는 표준적인 방법이 있음을 알 수 있다.즉, 타입의 기능이 있다.

$(A=B)\to(A\simeq B),}$

$이$는 A${\displaystyle }$, ${\displaystyle B}$ ${\displaystyle A,B}$ 유형이 동일하며$$, 특히 동등하다는 것을 나타낸다.null

단발성 공리는 이 함수 자체가 동등하다고 말한다.^{[27]: 115} 그러므로, 우리는

$(A=B)\simeq(A\simeq B)}$

"다시 말해 정체성은 등가성에 해당된다.특히 '등등유형은 동일하다'고 말할 수도 있다."^{[27]: 4}

적용들

정리증거

HoTT는 수학적인 증명들이 컴퓨터 증명 보조자들을 위한 컴퓨터 프로그래밍 언어로 이전보다 훨씬 더 쉽게 번역될 수 있도록 한다.이 접근법은 컴퓨터가 어려운 증거를 확인할 수 있는 가능성을 제공한다.^[35]null

수학의 한 가지 목표는 사실상 모든 수학적 이론이 모호하지 않게 도출되고 증명될 수 있는 공리를 공식화하는 것이다.수학에서 올바른 증거는 논리의 법칙을 따라야 한다.그것들은 공리와 이미 입증된 진술로부터 오류 없이 파생될 수 있어야 한다.^[35]null

HoTT는 논리-수학적 명제의 동일성을 호모토피 이론에 관련시키는 단발성 공리를 추가한다."a=b"와 같은 방정식은 서로 다른 두 기호가 같은 값을 갖는 수학 명제다.호모토피형 이론에서 이것은 기호의 값을 나타내는 두 모양이 위상학적으로 동등하다는 의미로 받아들여진다.^[35]null

ETH Zürich Institute for 이론 연구 책임자인 Giovanni Felder는 이러한 위상학적 동등성 관계는 보다 포괄적이기 때문에 호모토피 이론에서 더 잘 공식화될 수 있다고 주장한다.호모토피 이론은 "a와 b"가 왜 같은지 뿐만 아니라 이것을 어떻게 도출하는지도 설명한다.세트 이론에서, 이 정보는 추가로 정의되어야 할 것이며, 이것은 수학적 명제를 프로그래밍 언어로 번역하는 것을 더 어렵게 만든다.^[35]null

컴퓨터 프로그래밍

이 구간은 확장이 필요하다.덧셈으로 도와줘도 된다. (2014년 12월)

2015년을 기점으로 호모토피형 이론에서 단발성 공리의 연산 행동을 모델링하고 공식적으로 분석하기 위한 강도 높은 연구 작업이 진행되고 있었다.^[36]null

입체형 이론은 호모토피형 이론에 연산적인 내용을 부여하기 위한 하나의 시도다.^[37]null

그러나, 준-심층형과 같은 특정한 물체는 정확한 평등의 어떤 개념에 근거하지 않고서는 건설될 수 없다고 여겨진다.따라서 그 유형을 경로를 존중하는 섬유유형과 그렇지 않은 비섬유유형으로 나누는 다양한 2단계 유형 이론이 개발되었다.데카르트 입체 계산형 이론은 호모토피형 이론에 완전한 계산적 해석을 제공하는 최초의 2차원 유형 이론이다.^[38]null

참고 항목

• 건축 미적분학
• 커리-하워드 통신
• 직감형 이론
• 호모토피 가설
• 단발적 기초

참조

참고 문헌 목록

추가 읽기

• 데이비드 코필드(2020), 모달 호모토피 유형 이론: 옥스퍼드 대학 출판부의 새로운 철학 논리의 전망

외부 링크

위키미디어 커먼즈에는 호모토피형 이론과 관련된 미디어가 있다.

• 호모토피형 이론
• nLab에서의 호모토피형 이론
• 호모토피형 이론 위키
• Vladimir Voevodsky의 Univalent Foundation 웹페이지
• 호모토피형 이론과 스티브 어오디의 수학의 비범한 기초
• "건설형 이론과 호모토피" – Steve Awodey의 고등연구기관 비디오 강의

정형화된 수학의 도서관