핵심 개념
이 논문은 (co)카르테시안 화살표, 섬유화, 함수자에 대한 일반화된 처리를 제공합니다. 고전적인 조건과 달리, 종단점 포함은 임의의 모양 포함으로 대체됩니다. 이 프레임워크는 합성 내부 (∞, 1)-범주 이론의 개발을 지원하는 Riehl–Shulman의 심플리셜 호모토피 타입 이론입니다.
초록
이 논문은 (co)카르테시안 화살표, 섬유화, 섬유화 함수자에 대한 일반화된 처리를 제공합니다. 고전적인 조건과 달리, 종단점 포함은 임의의 모양 포함으로 대체됩니다. 이 프레임워크는 Riehl–Shulman의 심플리셜 호모토피 타입 이론으로, 합성 내부 (∞, 1)-범주 이론의 개발을 지원합니다.
서론
우리는 셀, 섬유화, 섬유화 함수자에 대한 공식 조건을 연구합니다. 이는 잘 알려진 코카르테시안 섬유화 이론을 일반화합니다.
우리는 Riehl–Shulman의 심플리셜 호모토피 타입 이론 설정에서 작업합니다. 이는 컴퓨터 공식화에 적합한 합성 (∞, 1)-범주 이론 프레임워크를 제공합니다.
우리의 조건은 2-범주 내부에서 섬유화를 특성화하는 데 전통적으로 사용되었던 쉐발레 조건을 일반화합니다.
우리의 작업은 코카르테시안 화살표, 섬유화, 함수자에 대한 특성화 정리가 그들의 좌측 보조 우측 역 조건에 의한 특성화로부터 형식적 결과라는 것을 명확히 합니다.
전제
의존 타입 이론의 기초에서 작업합니다.
유니발런스 공리를 가정합니다.
타입의 호모토피 이론에 대해 설명합니다.
심플리셜 호모토피 타입 이론을 소개합니다. 이는 합성 (∞, 1)-범주 이론을 포착하기 위해 표준 HoTT를 확장합니다.
심플리셜 (∞, 1)-범주 이론의 합성 개념을 설명합니다.
섬유화 (∞, 1)-범주 이론에 대해 논의합니다.