The $\infty$-category of $\infty$-categories in simplicial type theory

기술 요약: 심플리셜 유형론(Simplicial Type Theory)에서의 $\infty$-범주로서의 $\infty$-범주

문제 제식 (Problem Statement)
Riehl과 Shulman이 도입한 심플리셜 유형론(STT)은 유향 구간(directed interval) $I$를 호모토피 유형론(HoTT)에 확장함으로써 $(\infty, 1)$-범주론을 위한 합성적(synthetic) 프레임워크를 제공한다. STT는 $\infty$-범주를 특정 성질(Segal 및 Rezk 조건)을 만족하는 유형으로 성공적으로 정의하며, 극한, 여극한, 그리고 파이버 범주(fibered categories)와 같은 구성을 지원한다. 그러나 근본적인 간극이 존재했다: 유형의 유니버스 $U$ 자체가 STT 내에서 $\infty$-범주가 되지 않는다는 점이다. 구체적으로, $\infty$-범주 술어($\text{isCat}$)를 만족하는 유형의 부분 유형(subtype)은 합성적 사상(synthetic morphisms, 함수 $I \to \sum_{A:U} \text{isCat}(A)$)이 합성되거나 펑터를 충실하게 표현하지 못하기 때문에 범주를 형성하지 못한다. 결과적으로, "범주의 범주"($\text{Cat}$)가 유니버스의 구성 가능한 부분 유형으로서 존재할 것이라는 추측이 있었으나 실현되지 못했다. 이러한 부재는 straightening–unstraightening 정리의 내재화를 방해하고, 유향 유형론(directed type theory)을 고차 대수적 구조에 적용하는 데 걸림阻이 되었다.

방법론 (Methodology)
저자들은 큐비컬 유형론(cubical type theory)과 모달 의존 유형론(modal dependent type theory, MTT)의 기법을 심플리셜 유형론의 맥락에 적응시켜 $\text{Cat}$을 구축한다. 방법론은 다음과 같은 핵심 단계로 진행된다:

1. 삼각 유형론 ($TT^\triangle$): 저자들은 유향 구간 $I$가 전순서 집합(totally ordered set)이 아닌 유계 분배 래티스(bounded distributive lattice)인 $TT^\triangle$ 내에서 작업한다. 이 모델(Dedekind cubical spaces)은 지수 함수 $I \to (-)$에 대한 "놀라운 우측 부적(amazing right adjoint)"을 허용하는데, 이는 표준 심플리셜 공간에는 결여되어 있으나 보편적 파이버(universal fibrations)를 정의하는 데 결정적인 특징이다.
2. 모달리티 (Modalities): 이론은 $\flat$ 모달리티(이산 펑터)와 $\sharp$ 모달리티(코이산 펑터)를 포함한 모달리티로 확장된다. 이를 통해 전역 원소(global elements)를 내재화하고 이산 그로이데이드(discrete groupoids)와 일반적인 범주를 구분할 수 있다.
3. 보편적 코카르테시안 가족 (Universal Cocartesian Family): Licata 외 연구자들과 Weaver 및 Licata의 방식을 따라, 저자들은 $\text{Cat}$을 유형에 대한 직접적인 술어가 아니라 보편적 코카르테시안 가족의 기저(base)로 정의한다. 저자들은 $I^n$ 상에 정의된 술어(예: inner fibration 또는 locally cocartesian lifts를 가짐)를 유니버스 $U$ 상의 술어로 전치(transpose)하기 위해 보조정리 2.9를 활용한다.
4. $\text{Cat}$의 정의: $\text{Cat}$은 Rezk 조건을 만족하고, inner(상대적 Segal 조건을 만족함)하며, 합성 가능한 locally cocartesian lifts를 갖는 유형들로 구성된 $U$의 부분 유형으로 정의된다.
5. 유향 단일성 (Directed Univalence): 저자들은 $\text{Cat}$이 "유향 단일성" 원리를 만족함을 증명하여, $\text{Cat}$ 내의 합성적 사상과 $\flat$ 모달리티를 매개로 한 기저 유형들 사이의 함수 간의 동등성을 확립한다.

핵심 기여 및 결과 (Key Contributions and Results)

• $\text{Cat}$의 구축: 본 논문의 주요 기여는 STT 내에서 $\infty$-범주의 $\infty$-범주를 최초로 구축한 것이다. 저자들은 $\text{Cat}$을 유의 부분 유형으로 정의하고, 그것이 그 자체로 범주(즉, simplicial, Segal, Rezk 조건을 만족함)임을 증명한다.
• 보편적 성질 (정리 4.2): 본 논문은 $\text{Cat}$이 보편적 코카르테시안 가족의 기저임을 확립한다. 임의의 범주 $C$(구체적으로 $\flat$-annotated된)에 대하여 다음의 동등성이 존재한다:
  $$\langle \flat \mid C \to \text{Cat} \rangle \simeq \langle \flat \mid \sum_{E: C \to U} \text{isCocart}(E) \rangle$$
  이는 Grothendieck 대응(straightening–unstraightening)을 순수하게 유형론적으로 특징짓는다.
• 유향 단일성 (따름정리 5.5): 저자들은 $\text{Cat}$의 $\flat$-원소 $A, B$에 대하여, 합성적 사상의 유형이 그들 사이의 함수의 유형와 동등함을 증명한다:
  $$\text{hom}_{\text{Cat}}(A, B) \simeq \langle \flat \mid A \to B \rangle$$
  이 결과는 $\text{Cat}$을 (이산 범주로서의) 공간의 범주와 구별시킨다. 공간의 경우, 이 동등성은 $\flat$ 모달리티 없이 성립한다.
• 합성적 Straightening–Unstraightening: unstraightening 사상 $U: (C \to \text{Cat}) \to \text{Cat}/C$의 파이버를 분석함으로써, 저자들은 Lurie의 straightening–unstraightening 정리에 대한 완전한 합성적 증명을 제공한다. 그들은 이 사상의 상(image)이 정확히 코카르테시안 가족과 코카르테시안 펑터로 구성됨을 보여준다.
• 구조 준형 원리 (Structure Homomorphism Principle, SHP): 이 구축은 유향 버전의 구조 동일성 원리를 위한 새로운 예시들을 가능하게 한다. 저자들은 $\text{Cat}$을 유형론적 연결자(connectives) 및 모달리티와 결합하여 모노이달 범주(monoidal categories) 및 마크된 범주(marked categories)와 같은 복잡한 범주를 구성하는 방법을 보여준다.

의의 및 주장 (Significance and Claims)
본 논문은 심플리셜 유형론의 근간에 있는 주요 간극을 메운다고 주장한다. $\text{Cat}$을 구축함으로써 저자들은 다음을 가능하게 한다:

1. 고차 범주론의 내재화: 이전에 외부 모델 범주론적 논증을 필요로 했던 주요 기초적 결과들을 이제 유형론 내에서 합성적으로 증명할 수 있다.
2. 유향 유형론의 의미론: $\text{Cat}$의 존재는 "완전하게 유향된(fully directed)" 유형론들을 STT로 합성적으로 번역할 수 있게 하여, $\infty$-범주를 적절히 포착하는 모델을 제공한다.
3. 새로운 구성: 이 프레임워크는 복잡한 대수적 구조(예: $E_1$-모노이드, 모노이달 범주)를 정의하고, Quillen의 K-군(K-groups) 정의를 통해 대수적 K-이론 개념을 합성적 환경 내에서 적용하는 것을 용이하게 한다.

저자들은 자신들의 접근 방식이 ( $TT^\triangle$의 공리들에 의존하며) 유도 과정에서 모델 독립적(model-independent)인 동시에, 큐비컬 공간의 모델에 의해 검증됨을 강조한다. 저자들은 이 연구를 고차 대수 및 오퍼라드(operad) 이론을 합성적으로 구현하기 위한 단계로 보며, $\text{Cat}$의 구축은 완료되었으나 대수적 K-이론에 대한 응용을 완전히 탐구하고 이론의 계산적 설명(computational account)을 개발하기 위한 추가적인 작업이 필요함을 언급한다.