Univalent Enriched Categories and the Enriched Rezk Completion

기술 요약: 유니발런트 인리치드 카테고리와 엔리치드 레즈크 완결(Rezk Completion)

문제 정의
범주론은 수학과 컴퓨터 과학의 기초적인 프레임워크이며, 인리치드 카테고리(enriched categories)는 고차 범주론, 호모토피 이론, 그리고 효과적인 언어(예: DCPO를 사용하는 효과적 언어)의 의미론에서 중요한 역할을 한다. 그러나 유니발런트 파운데이션(Univalent Foundations, Homotopy Type Theory)의 맥락에서, 표준적인 범주 정의는 동형 객체들이 구별 불가능해야 한다는 동형 원리(principle of equivalence)를 만족하지 못하는 경우가 많다. "유니발런트 범주"(동형성이 객체의 동일성과 동등한 유니발런트 범주)는 일반적인 범주에 대해서는 확립되어 있지만, 유니발런트 인리치드 카테고리의 이론은 아직 미발달 상태이다. 구체적으로, 구조 동일성 원리(structure identity principle), 동등성(equivalences)의 특징화, 그리고 인리치드 카테고리에 대한 레즈크 완결(Rezk completion, 즉 유니발런트 반사)의 존재에 관한 정식화된 결과가 부족하다. 또한, 클레이슬리 범주(Kleisli categories)와 같은 표준적인 구성들은 유니발런트하지 않은 경우가 많으므로, 인리치드 설정 내에서 유니발런트한 유사체를 구성하기 위한 방법이 필요하다.

방법론
본 논문은 UniMath 라이브러리를 사용하여 Rocq 증명 보조기 내에서 인리치드 범주 이론을 개발하며, 이는 유니발런트 파운데이션을 준수한다. 핵심적인 방법론적 접근 방식은 다음과 같다:

1. 구조로서의 인리치먼트(Enrichments as Structure): 인리치드 카테고리를 객체와 호무-객체(hom-objects)의 집합(Kelly의 정의)으로 정의하는 대신, 저자들은 이를 인리치먼트가 결합된 범주로 정의한다. 인리치먼트는 모노이달 범주 $\mathcal{V}$ 내의 호무-객체, 항등 및 합성 사상, 그리고 범주 내의 모피즘과 호무-객체의 원소 사이의 대응 관계를 포함한다. 이러한 관점은 인리치드 카테고리를 추가적인 구조를 가진 유니발런트 범주로 취급한다.
2. 디스플레이드 비카테고리(Displayed Bicategories): 구조 동일성 원리를 증명하기 위해, 저자들은 디스플레이드 비카테고리 기법을 활용한다. 저자들은 유니발런트 범주($UnivCat$)의 비카테고리 위에 디스플레이드 비카테고리$dEnrichCat_{\mathcal{V}}$를 정의한다. 이 디스플레이의 전체 비카테고리(total bicategory)는 $EnrichCat_{\mathcal{V}}$이다. 이를 통해 $UnivCat$에 대한 기존의 유니발런스 결과를 인리치드 설정의 유니발런스를 증명하는 데 재사용할 수 있다.
3. 직교 인수 분해 시스템(Orthogonal Factorization Systems): 동등성을 특징화하기 위해, 본 논문은 비카테고리에서의 직교 인수 분해 시스템을 채택한다. 저자들은 완전 충실(fully faithful) 및 본질적 전사(essentially surjective) 인리치드 함자를 정의하고, 이들이 직교 인수 분해 시스템을 형성함을 증명한다.
4. 두 가지 레즈크 완결 구성: 인리치드 카테고리의 레즈크 완결을 위한 두 가지 구별된 구성을 제공한다:
   • 요네다 임베딩(Yoneda Embedding): 완결을 요네다 임베딩의 상으로 구성한다. 이는 $\mathcal{V}$가 완비(complete)이고 대칭 모노이달 폐(symmetric monoidal closed)여야 하지만, 표준적인 범주론에 의존한다.
   • 고차 귀납적 타입(Higher Inductive Types, HITs): HIT의 제거 규칙(elimination rules)을 사용하여 하부 범주의 레즈크 완결에 인리치먼트를 부여함으로써 완결을 구성한다. 이 접근 방식은 $\mathcal{V}$의 완비성이나 폐쇄성에 대한 가정을 피하며, 유니버스가 HIT에 대해 닫혀 있다면 유니버스 레벨을 보존한다.
5. 보편 성질(Universal Properties): 본 논문은 인리치드 카테고리의 레즈크 완결에 대한 보편 성질을 확립하며, 약한 동등성(weak equivalence, 즉 완전 충실하고 본질적 전사인 함자)에 의한 전치(precomposition)가 함자 범주들 사이의 인접 동등(adjoint equivalence)을 유도함을 입증한다.

주요 기여 및 결과

• 구조 동일성 원리: 본 논문은 유니발런트 인리치드 범주들의 비카테고리($EnrichCat_{\mathcal{V}}$)가 유니발런트임을 증명한다(정리 2.8). 이는 두 유니발런트 인리치드 범주 사이의 항등 타입이 그들 사이의 인접 동등의 타입과 동등함을 의미한다.
• 동등성의 특징화: 모든 인리치드 함자가 완전 충실하고 본질적으로 전사적이면 인접 동등임을 증명한다(정리 4.8). 이 결과는 구성적이며, 선택 공리 없이 유니발런트한 도메인과 코도메인을 활용한다.
• 레즈크 완결: 인리치드 카테고리를 위한 두 가지 레즈크 완결 구성을 제공한다(구성 5.5 및 5.7). 본 논문은 모든 인리치드 범주가 레즈크 완결을 가지며, 약한 동등성을 따라 유니크하게 확장되는 유일한 함자를 갖는다는 보편 성질을 만족함을 증명한다(정리 5.2).
• 유니발런트 클레이슬리 범주: 유니발런트 인리치드 클레이슬리 범주를 구성한다. 저자들은 표준 클레이슬리 범주 $K(T)$와 그 유니발런트 대응물인 $Kleisli(T)$(Eilenberg-Moore 범주의 완전 부분 범주로서)를 정의한다. 레즈크 완결과 보편 성질을 사용하여, $Kleisli(T)$가 유니발런트 인리치드 범주에서의 클레이슬리 대상의 보편 성질을 만족함을 보인다(구성 6.9).
• 예시 및 특징화: 자기 인리치먼트(self-enrichment), 반대 인리치먼트(opposite enrichments), 그리고 베이스 변경(changes of base)을 포함한 다양한 예시를 제공한다. 또한 카테시안 구조(예: DCPO)에 대한 인리치먼트를 특징화하고, 포인티드 세트(pointed sets)와 포셋(posets)을 다루기 위해 "스매시 곱을 지원하는 폐쇄 구조"라는 개념을 도입하지만, 포인티드 DCPO에 대한 한계를 언급한다.

의의 및 주장
본 논문은 유니발런트 파운데이션 내에서 인리치드 범주론을 위한 견고한 기초를 확립한다고 주장한다. 주요 의의는 다음과 같다:

1. 정식화: 이전에 일반 범주에 비해 광범위한 정식화가 부족했던 인리치드 범주를 위한 Rocq/UniMath 라이브 libraries를 제공한다.
2. 개념의 정확성: 인리치드 범주를 (인리치먼트를 통한) 추가 구조를 가진 유니발런트 범주로 보는 관점이 구조 동일성 원리와 같은 근본적인 성질의 증명을 단순화함을 보여준다.
3. 비유니발런스 문제 해결: 클레이슬리 범주와 같은 일반적인 구성들이 본질적으로 유니발런트하지 않다는 문제를, 필요한 보편 성질을 보존하는 유니발런트 버전을 얻기 위한 체계적인 방법(레즈크 완결)을 제공함으로써 해결한다.
4. 기초 도구: 유니발런트 비카테고리로서 유니발런트 인리치드 범주들의 비카테고리를 확립하며, 이는 유니발런트 환경에서 더 발전된 내부 범주론(예: 모나드, 리미트)을 개발하기 위한 전제 조건이다.

저자들은 자신들의 접근 방식이 많은 표준적인 경우를 다루지만, 적절한 범주가 아닌 세트에서 몫(quotient)을 취해야 하는 특정 구조(예: 포인티드 DCPO)의 스매시 곱에 대해서는 한계가 있다고 언급한다. 이들은 향후 연구가 인리치드 범주의 장비(equipment)를 개발하거나, 이러한 사례들을 처리하기 위해 스매시 곱 개념을 일반화하는 방향이 될 수 있음을 시사한다.