다항식 함수(타입 이론)

이 기사는 다른 어떤 관련 기사도 없기 때문에 고아이다.관련 기사에서 이 페이지에 대한 링크를 소개하십시오. Find link 툴에서 제안 사항을 확인하십시오. (2018년 3월)

유형 이론에서 다항식 펑터(또는 용기 펑터)는 유도형 및 공유도형의 개념과 밀접하게 관련된 유형의 범주의 일종의 엔드펀터이다.구체적으로는 모든 W타입(resp).M형)은 이러한 함수의 초기 대수(resp. final colgebras)이다.

다항식 함수는 ^[1]δ-유형을 가진 프리오포의 보다 일반적인 설정에서 연구되었다. 이 논문은 마틴-뢰프 스타일 유형 이론의 유형 범주 내에서만 이 개념의 적용을 다룬다.

정의.

허락하다U타입의 세계다.A:U, 그리고,B:A→U에 의해 색인화된 종류의 과이다A쌍(A,B)는 시그니처^[2] 또는 컨테이너라고 ^[3]불리기도 합니다.용기에 연결된 다항식 함수(A,B)의 정의는 다음과 같습니다.^[4][5][6]

$${\displaystyle\begin\aligned}P:U&\long rightrow U&\longmap to \sum _{a:A}(B(a)\to X)\end {aligned}.}$$

모든 펑터는 자연히 다음과 같다.P컨테이너 ^[7]펑터라고 불립니다.의 동작P함수에 대한 정의는 다음과 같습니다.

$$디스플레이 스타일P^{*}:(X\to Y)&\rong rightarrow(P^{*}X\to P^{*}Y)\\(f,(a,g))&\longmapsto(a,g\longf)\end{aligned}).}$$

이 할당은 확장 유형 이론에서만 기능하는 것이 아닙니다(#프로퍼티 참조).

특성.

집중형 이론에서, 그러한 함수는 진정한 함수가 아니다. 왜냐하면 우주형은 엄밀하게 범주가 아니기 때문이다.그러나 명제적 등가까지 기능한다.즉, 다음과 같은 정체성이 존재한다.

$$디스플레이 스타일P^{*}(f\circ g)&=P^{*}f\circ P^{*}g\\P^{*}({\mathsf {id}_{X})&=mathsf {id}_{PX}\end{aligned}).}$$

모든 기능에 대해f그리고.g및 모든 유형X${\displaystyle {\mathsf{여기}}_{}}$서 $i{\displaystyle {\mathsf{}}_{}}$ ${\displaystyle d_{}}$ X$({$})는$$ 타입의 아이덴티티 함수입니다.X를 클릭합니다.^[8]

인라인 따옴표

레퍼런스

• Univalent Foundations Program (2013). Homotopy Type Theory: Univalent Foundations of Mathematics. Institute for Advanced Study. p. 159.
• Awodey, Steve; Gambino, Nicola; Sojakova, Kristina (2012-01-18). "Inductive types in homotopy type theory". arXiv:1201.3898 [math.LO].
• Awodey, Steve; Gambino, Nicola; Sojakova, Kristina (2015-04-21). "Homotopy-initial algebras in type theory". arXiv:1504.05531 [math.LO].
• Ahrens, Benedikt; Capriotti, Paolo; Spadotti, Régis (2015-04-12). Non-wellfounded trees in Homotopy Type Theory. Leibniz International Proceedings in Informatics (LIPIcs). Vol. 38. pp. 17–30. arXiv:1504.02949. doi:10.4230/LIPIcs.TLCA.2015.17. ISBN 9783939897873. S2CID 15020752.
• Abbott, Michael; Altenkirch, Thorsten; Ghani, Neil (2005). "Containers: Constructing strictly positive types". Theoretical Computer Science. 342 (1): 4. doi:10.1016/j.tcs.2005.06.002.

외부 링크

• 다항식 함수에 대한 광범위한 노트 모음