The Leibniz adjunction in homotopy type theory, with an application to simplicial type theory

기술 요약: 호모토피 유형론에서의 라이브니츠 수반(Leibniz Adjunction)

문제 정의
심플리셜 유형론(Simplicial Type Theory, STT)은 간격(interval)을 통해 유형에 방향성 모포즘(directed morphisms)을 부여함으로써 호모토피 유형론(HoTT)을 확장하여 고차 범주를 위한 합성적 프레임워크를 제공한다. 핵심적인 과제는 방향성 모포즘을 합성할 수 있는 "세갈 유형(Segal types)"을 정의하는 것이다. 합성은 직관적이지만, 이 합성이 결합 법칙(associativity)과 항등 법칙(unitality)을 만족하도록 보장하기 위해서는 무한한 고차 일관성(higher coherences)의 계층이 필요하다. Riehl과 Shulman에 의한 표준적인 STT 정식화에서 이러한 일관성들은 종종 메타 이론적 구성(meta-theoretic constructions)을 통해 처리되는데, 이는 완전한 형식화를 어렵게 만든다. 구체적으로, $(2,1)$-혼(horn)에 대해 유일한 필러(unique fillers)를 갖는 유형(즉, 세갈 유형의 기본 조건)이 모든 내부 $(n,k)$-혼(내부 결합 법칙과 항등 법칙을 일반화한 것)에 대해 유일한 필러를 가짐을 증명하는 것은 쉽지 않다. Riehl과 Shulman의 이전 결과들은 특정 저차원 사례($n=3$)만을 다루었으나, 통합된 HoTT 프레임워크 내에서 모든 $n$과 $k$에 대해 일반적인 증명을 제시하는 것은 미해결된 기술적 난제였다.

방법론
저자들은 Riehl과 Shulman의 메타 이론적 간격 접근 방식 대신, Gratzer, Weinberger, Buchholtz를 따르는 "평범한(plain)" 호모토피 유형론 접근 방식을 채택한다. 이들은 총 순서(total orders)나 특정 모달리티(modalities)를 요구하지 않는 유계 분배 격자(bounded distributive lattice)를 형성하는 간격 유형 $I$를 가정한다.

핵-기술적 혁신은 "와일드 범주(wild category)의 유형들" 내에서 **라이브니츠 수반(Leibniz adjunction)**을 내재화하는 것이다.

1. 와일드 범주(Wild Categories): 저자들은 범주론을 HoTT로 나이브하게 번역한 "와일드 범주"를 다룬다. 이들은 고차 일관성 데이터(결합 법칙과 항등 법칙이 정의적으로 성립하거나 추적되지 않음)가 부족하며, 이로 인해 $(\infty, 1)$-범주와는 구별되지만 저자들의 목적에는 충분하다.
2. 수반(The Adjunction): 저자들은 푸시아웃-곱(pushout-product, $\hat{\times}$로 표기)이 와일드 범주의 사상(maps)에서 풀백-홈(pullback-hom, $\pitchfork$로 표기)의 좌수반임을 확립한다.
   • 사상 $f: A \to B$와 $g: X \to Y$에 대하여, 푸시아웃-곱 $f \hat{\times} g$는 $f \times Y$와 $A \times g$의 푸시아웃으로부터 유도된 사상이다.
   • 풀백-홈 $f \pitchfork g$는 함수 유형들 사이의 유도된 사상이다.
   • 이 수반은 $\text{Map}(f \hat{\times} g, h) \simeq \text{Map}(f, g \pitchfork h)$를 성립시킨다.
3. 사상 vs. 패밀리(Maps vs. Families): 와일드 범주의 사상(maps) 내에서의 직접적인 증명은 일관성 데이터(7-튜플의 사상과 식별들)를 추적하는 복잡성 때문에 다루기 어렵다. 이를 극복하기 위해, 저자들은 언벨런스 공리(univalence axiom)를 사용하여 와일드 범주의 사상과 와일드 범주의 패밀리(dependent types) 사이의 동치 관계를 확립한다. 그들은 푸시아웃-곱과 풀백-홈이 패밀리의 범주 내에서 파이버와인 조인(fiberwise join) 및 특정 의존적 곱(dependent product) 구성에 대응함을 증명하며, 이 과정에서 수반 관계를 검증하기가 더 용이해진다.

주요 기여 및 결과

1. 라이브니츠 수반 (정리 3.16): 본 논문은 푸시아웃-곱과 풀백-홈이 와일드 범주의 유형들에서 수반 쌍을 형성함을 증명한다. 이는 1-범주에서는 잘 알려져 있으나, 고차 구조(심지어 "와일드" 설정에서도)에 대해 이를 증명하려면 사상과 패밀리 사이의 동치 관계를 신중하게 다루어 다루기 힘든 일관성 추적을 피해야 하므로 중요한 기술적 결과이다.
2. 세갈 유형 속성의 일반화 (정리 4.9): 라이브니츠 수반을 사용하여, 저자들은 어떤 유형이 $(2,1)$-혼에 대한 유일한 필러를 가진다면(즉, 세갈 유형이라면), 자동으로 모든 내부 $(n,k)$-혼($0 < k < n$)에 대한 유일한 필러를 가짐을 증명한다.
   • 이는 $n=3$을 다루었던 Riehl과 Shulman의 결과를 일반화하며, 림(Lurie)의 결과를 심플리셜 유형론에 대해 제공한다.
   • 이 증명은 내부 혼 포함 관계 $\lambda^n_k$가 "내부 아노다인(inner anodyne)"(즉, 모든 세갈 유형에 대해 좌직교(left orthogonal)함)임을 보이는 것에 의존한다. 이는 $\lambda^n_k$가 $\lambda^n_k \hat{\times} \lambda^2_1$의 은닉(retract)임을 보여줌으로써 달성되며, 라이브니츠 수반으로부터 도출된 직교성의 폐쇄 성질을 적용하여 이루어진다.
3. 정식화(Formalization): 모든 결과는 Cubical Agda로 정식화되었다. 코드는 공개되어 있으며, 인덱스와 푸시아웃을 다루는 복잡한 조합론적 논증의 검증 역할을 한다.

의의 및 주장
본 논문의 주요 기여는 라이브니츠 수반을 HoTT 내에 성공적으로 내재화한 것이며, 이는 심플리셜 유형론에서 고차 일관성을 도출하기 위한 강력한 도구로 작용한다는 점이라고 주장한다.

• 합성적 프레임워크: 내부 간격 유형을 사용함으로써, 저자들은 모든 고차 일관성이 메타 이론적 양화(quantification)에 의존하지 않고 HoTT 내에서 합성적으로 기술되고 도출될 수 있음을 입증한다.
• 정식화 가능성: 저자들은 자신들의 접근 방식이 Agda에서의 완전한 정식화를 가능하게 한다고 강조한다. 그들은 Riehl-Shulman의 메타 이론적 접근 방식이 (메타 수준에서의 집합 기반 추론 덕분에) 정리의 진술을 더 쉽게 만들 수는 있지만, 그들의 내부 프레임워크 내에서 일반적인 경우의 증명은 비자명하며 일관성 추적에 관한 "압도적인 대부분의 과제"를 관리하기 위해 라이브니츠 수반의 개발이 필요했음을 언급한다.
• 기술적 유용성: 와일드 범주의 사상과 패밀리 사이의 동치는 푸시아웃-곱과 풀백-홈을 다루는 증명을 단순화하여 직교성 속성의 도출을 가능하게 하는 핵심적인 방법론적 도구로 제시된다.

요약하자면, 본 논문은 와일드 범주적 설정에서 라이브니츠 수반의 적용을 통해 기본적인 세갈 조건이 전체 고차 범주적 일관성을 함의함을 증명함으로써, 심플리셜 유형론을 위한 엄밀하고 정식화된 기초를 제공한다.