The internal languages of univalent categories

기술 요약: 유니발렌트 범주(Univalent Categories)의 내부 언어

문제 제기
범주 논리학에서의 내부 언어 정리들은 구문론(타입 이론)과 의미론(범주 모델) 사이의 동치 관계를 확립한다. Clairambault와 Dybjer [CD14]의 기념비적인 결과는 Seely의 원래 정리를 [See84] 교정하여, 국소적 카르테시안 폐 범주(LCCCs)의 이범주(bicategory)와 외연적 항등 타입(extensional identity types), $\Sigma$-타입, $\Pi$-타입을 지원하는 민주적 가족들의 범주(democratic categories with families, CwFs)의 이범주 사이의 이동치(biequivalence)를 확립하였다.

그러나 이 결과는 집합론적 기초 내에서 공식화되었다. 유니발렌트 기초(호모토피 타입 이론)에서 표준적인 CwF 개념은 근본적인 장애물에 직면한다: 유니발렌스 공리는 집합들의 타입이 그 자체로 집합이 아님(이는 1-type임)을 함의한다. 결과적으로 CwF에서 문맥(context) 내의 타입들의 모임이 집합이어야 한다는 요구 조건은 유니발렌트 집합 범주에 의해 위반된다. 또한, "선택된" 구조(예: split fibrations)와 "존재하는" 구조(예: isomorphism up to isomorphism인 극한) 사이의 구분은 집합론적 기초에서 선택 공리나 엄격화(strictification) 절차를 필요로 하는 코히어런스(coherence) 문제를 야기한다. 유니발렌트 기초에서는 동형(isomorphism)이 항등(identity)을 함의하므로 이러한 구분이 사라지지만, 기존의 CwF 프레임워크는 직접 적용될 수 없다.

방법론
본 논문은 유니발렌트 기초 내에서 **유니발렌트 범주(univalent categories)**와 **이해 범주(comprehension categories)**를 활용하여 범주적 의미론을 위한 새로운 프레임워크를 개발한다.

1. 유니발 l l e nt 범주: 저자는 대상들의 항등 타입이 동형 관계(adjoint equivalences)와 동치인 범주에서 작업한다. 이를 통해 adjoint equivalences를 항등으로 취급할 수 있어, 구조(예: 지수)의 보존에 관한 증명을 단순화하고 극한을 선택하기 위한 선택 공리의 필요성을 제거한다.
2. 이해 범주: 타입을 집합으로 요구하지 않고 의존 타입을 모델링하기 위해, 본 논문은 이해 범주(파이버레이션과 표시된 범주에 기반함)를 채택한다. 이해 범주는 문맥의 기저 범주, 타입들의 표시된 범주, 클리빙(substitution을 제공함), 그리고 이해 함자(comprehension functor)로 구성된다. 저자는 기저 범주와 표시된 범주가 모두 유니발렌트인 **유니발렌트 완전 이해 범주(univalent full comprehension categories)**에 주의를 집중한다.
3. 표시된 이범주(Displayed Bicategories): 모델들의 이범주를 구축하는 과정은 표시된 이범주 [AFM+21]에 크게 의존한다. 이 모듈형 접근 방식은 더 단순한 기저 이범주 위에 속성(예: 유한 극한, $\Pi$-타입, 유니버스)을 층층이 쌓음으로써 복잡한 이범주(예: LCCC 또는 toposes)를 구축할 수 있게 한다. 이러한 모듈성은 결과적인 이범주가 그 자체로 유니발렌트임을 증명하는 데 용이하다.
4. 국소적 성질(Local Properties): 유한 극한을 가진 범주에서 toposes와 같은 더 복렴한 구조로 결과를 확장하기 위해, 저자는 Maietti의 국소적 성질 [Mai05] 개념을 변형하여 사용한다. 국소적 성질이란 슬라이싱(slicing)에 대해 닫혀 있는 범주들에 대한 조건이다. 저자는 표시된 이범주 프레임워크 내에서 이를 형식화하여, 유한 극한(base case)으로부터 다양한 클래스의 toposes로 이동치(biequivalence)를 확장한다.
5. 재인덱싱 및 유니버스: 유니버스를 다루기 위해, 본 논문은 표시된 이범주의 재인덱싱(reindexing of displayed bicategories) 기법을 사용한다. 이 기술은 기저 범주로부터 표시된 범주로 이동치를 전달할 수 있게 하여, 엄격한 안정성 법칙(strict stability laws) 대신 isomorphism up to isomorphism(유니발렌트 범주에서는 identity가 됨)을 따르는 특정 타입 형성자($\Sigma, \Pi$, 자연수)에 대해 닫힌 유니버스를 정의할 수 있게 한다.

주요 기여
본 논문은 네 가지 주요 기여를 한다:

1. Clairambault-Dybjer의 유니발렌트 대응물: 저자는 유한 극한을 가진 유니발렌트 범주와 유니발렌트 완전 DFL(finite limit) 이해 범주 사이의 이동치를 구축한다. 이는 유한 극한을 가진 유니발렌트 범주의 내부 언어가 unit, binary product, $\Sigma$-타입을 갖는 외연적 Martin-Löf 타입 이론임을 확립한다.
2. 국소적 카르테시안 폐 범주로의 확장: 이 이동치는 $\Pi$-타입을 지원하는 DFL 이해 범주와 유니발렌트 국소적 카르테시안 폐 범주로 확장된다. 이는 유니발렌트 LCCC의 내부 언어가 $\Pi$-타입을 갖는 외연적 Martin-Löf 타입 이론임을 확인한다.
3. Toposes 및 유니버스로의 확장: 저자는 국소적 성질을 사용하여 다양한 클래스의 toposes(pretoposes, $\Pi$-pretoposes, elementary toposes, NNO를 가진 toposes)로 일반화한다. 나아가, 특정 타입 형성자(자연수, 부분 대상 분류자, 명제 리사이징, $\Sigma$-타입, $\Pi$-타입)에 대해 닫힌 유니버스를 이 범주들에서 정의함으로써, 유니버스를 가진 elementary toposes에 대한 이동치를 확립한다.
4. 정식화(Formalization): 모든 구성과 증명은 UniMath 라이브러리를 사용하는 Rocq 증명 보조기에서 정식화되어, 이론의 정확성을 보장하고 기계 검증된 참조를 제공한다.

결과
본 논문은 다양한 유니발렌트 범주 클래스에 대해, 그에 대응하는 유니발렌트 이해 범주 클래스와의 이동치가 존재함을 증명한다. 구체적으로:

• 유한 극한: 유한 극한을 가진 유니발렌트 범주 $\simeq$ DFL 이해 범주 (Unit, Product, Equalizer, $\Sigma$).
• LCCC: 유니발렌트 LCCC $\simeq$ $\Pi$-타입을 가진 DFL 이해 범주.
• Toposes: 유니발렌트 elementary toposes (NNO 유/무) $\simeq$ 상응하는 국소적 성질(예: 부분 대상 분류자, 분리된 합, 몫)을 가진 DFL 이해 범주.
• 유니버스: 특정 타입 형성자에 대해 닫힌 유니버스를 가진 유니발렌트 elementary toposes $\simeq$ 상응하는 폐쇄 조건을 만족하는 유니버스 객체를 가진 DFL 이해 범주.

본 논문은 이러한 유니발렌트 범주 클래스들에 대해 그 내부 언어가 외연적 Martin-Löf 타입 이론임을 입증한다. 유니발렌트 범주를 사용함으로써 split fibrations의 필요성을 제거하고, (substitution이 엄격하게 성립해야 하는) 집합론적 모델에서 발생하는 코히어런스 문제를 해결하며, isomorphism이 identity가 되기 때문에 구조를 더 자연스럽게 다룰 수 있다.

의의 및 주장
본 논문은 자신의 연구가 의존 타입 이론의 의미론에 대한 새로운 관점을 제공한다고 주장한다. 유니발렌트 범주를 활용함으로써, 저자는 건전성(soundness)을 보장하기 위해 집합론적 기초에서 필요한 split fibrations와 선택 공제의 기술적 오버헤드를 피한다. 유니발렌트 기초에 내재된 구조 항등 원리는 대상들이 엄격한 equality가 아닌 equivalence까지 식별되는 범주적 구조를 더 자연스럽게 다룰 수 있게 한다.

저자는 본 연구에서 구문(syntax)이나 초기 모델(initial model)을 직접 구축하는 것이 아니라, 범주적 측면(모델들 사이의 동치)에 집중하고 있음을 명시한다. 저자는 이해 범주가 유니발렌트 기초에 적합하지만, CwF와 같은 다른 구조들은 타입에 대한 집합 제한(set-restriction) 때문에 적합하지 않다고 언급한다. 본 논문은 유니발렌트 범주적 구조와 타입 이론 사이의 견고하고 기계 검증된 대응 관계를 확립함으로써, 유니발렌트 기초가 이전의 결함 있는 집합론적 정식화 없이도 이러한 내부 언어 정리를 자연스럽게 지원함을 보여주는 기초적인 단계로 자리매김한다.