Extension Types for Free

기술 요약: 자유로운 확장 타입: 2-레벨 유형 이론에서의 코피브레이션(Cofibrations), 글루잉(Gluing), 그리고 유니밸런스(Univalence)

문제 제기
확장 타입(Extension types)은 의존 유형 이론(dependent type theory)의 근본적인 개념로, 고정된 끝점을 가진 경로(cubical type theories)나 하위 형상(subshapes) 위에 항이 고정되는 Riehl과 Shulman의 심플리셜 유형 이론(simplicial type theory), 또는 제어된 언폴딩(controlled-unfolding) 메커니립 등 다양한 맥락에서 등장한다. 기존 프레임워크에서 이러한 타입들은 대개 새로운 프리미티브(primitives)로서 상정되며, 이들의 형성 및 규칙을 규정하는 메타 이론적인 "페이스 칼큘러스(face calculus)" 또는 형상 층(shape layer)에 의해 통제된다. 이러한 접근 방식은 규칙을 검증하기 위해 특정 모델 구성이나 공리적 추가(엄격한 경계 조건, 상대적 함수 외연성, 호모토피 확장 성질 등)를 요구하는 경우가 많다. 호모토피 유형 이론(HoTT)의 핵심적인 미결 과제 중 하나는 "book HoTT"(HoTT book의 공리적 정식화)와 큐비컬 유형 이론(cubical type theories) 사이의 정확한 관계, 특히 두 이론이 서로 보수적 확장(conservative extensions)인지 여부를 결정하는 것이다.

방법론
본 논문은 이를 위한 통합 프레임워크로서 **2-레벨 유형 이론(Two-Level Type Theory, 2LTT)**을 활용한다. 2LTT는 HoTT를 "엄격한(strict)" (외부) 레벨의 동등성으로 풍부하게 만드는데, 이 외부 레벨은 일치성 증의 유일성(Uniqueness of Identity Proofs, UIP)과 함수 외연성(function extensionality)을 만족하며, "내부(inner)" (fibrant) 레벨은 표준적인 호모토피 구조를 유지한다.

• 의미론(Semantics): 이 프레임워크는 의미론적으로 "자유(free)"롭다. 표준적인 HoTT 모델(예: simplicial sets, cubical sets)은 프리쉬프(presheaf) 구성을 통해 자동으로 2LPT의 모델이 된다. 이 이론은 내부 레벨에 대해 보수적(conservative)이다. 즉, 내부 언어에서 증명할 수 없는 새로운 정리가 내부 레벨에서 새롭게 증명되지 않는다.
• 확장 타입의 정의: 확장 타입을 상정하는 대신, 본 논문은 이를 2LTT 내부에서 정의한다. 코피브레이션 $i: \Phi \hookrightarrow \Psi$ (외부 레벨에서의 사상), $\Psi$ 위의 fibrant 패밀리 $A$, 그리고 부분 섹션(partial section) $a$가 주어졌을 때, 확장 타입은 $a$에 대한 제한 사상의 **엄격한 파이버(strict fiber)**로 정의된다:
  $$\Pi_\Psi A \mid_i^a \coloneqq \Sigma_{f : \Pi_\Psi A} (f \circ i =_s a)$$
  여기서 $=_s$는 외부 레벨의 엄격한 동등성을 나타낸다.
• 코피브레이션(Cofibrations): "페이스 칼큘러스"는 외부 레벨에서의 코피브레이션 클래스로 대체된다. 본 논문은 어떤 사상이 코피브레이션인지에 대한 구체적인 선택을 매개변수로 취급하여, 핵심 정의를 변경하지 않고도 프레임워크가 다양한 설정(심플리셜, 큐비컬 등)에 적응할 수 있도록 한다.

주요 기여 및 결과

1. "자유로운" 확장 타입:
   본 논문은 2LTT에서 Riehl과 Shulman이 제안한 확장 타입의 전체 칼큘러스가 공리화되는 것이 아니라 정의 가능하다는 것을 보여준다.

   • 엄격한 규칙: 도입, 제거, $\beta$, $\eta$, 그리고 경계 규칙은 구조적으로 엄격하게 성립한다.
   • 증명 가능한 공리: 다른 설정에서 공리로 상정되었던 **상대적 함수 외연성(relative function extensionality)**과 호모토피 확장 성립(homotopy extension property, realignment) 등의 공리는 2LTT의 코피브레이션과 피브레이션의 성질로부터 유도되는 정리(theorem)가 된다.
   • 통합: 이 단일 정의는 큐비컬 경로, Riehl-Shulman 확장 타입, 그리고 명제 지표 타입(proposition-indexed types, 제어된 언폴딩)을 포함한 다양한 기존 사례들을 포괄한다.

2. 글루잉(Gluing)과 유니밸런스(Univalence)의 동치성:
   본 논문은 2LTT 프레임워크 내에서 큐비컬 글루잉과 유니밸런스 공리를 연결하는 정밀한 함의 순환 구조를 확립한다.

   • 유니밸런스 $\implies$ 글루잉: 내부 유니버스가 유니밸런트하다면, 임의의 코피브레이션에 대해 "Glue 데이터"(Glue 타입을 형성하는 데 필요한 구조)의 타입는 **수축 가능(contractible)**하다. 이는 호모토피 형태의 규칙을 만족하는 Glue 구조의 존재를 의미한다.
   • 글루잉 $\implies$ 유니밸런스: 반대로, "약한 Glue 구조"(경계 일치를 위해 내부 동등성만을 요구하고 경로 인터벌 구조를 갖는 구조)의 존재는 유니버스가 유니밸런트함을 함의한다.
   • 결과: 경로 인터벌(path interval)이 존재할 때, 유니밸런스와 수축 가능한 Glue 데이터의 존재는 서로 동치이다. 이는 표준적인 함의 방향(Glue 타입이 유니밸런스를 함의한다는 방향)을 역전시키며, 양방향 동치를 확립한다.

3. 정식화(Formalization):
   섹션 2부터 섹션 5까지의 모든 결과는 --two-level 플래그를 사용하여 Agda로 자동 정식화되었다. 이 정식화는 내부 HoTT 논증과 외부의 엄격한 레벨에 대한 추론을 결합하여, 이론적 주장의 일관성과 정확성을 검증한다.

4. 보수성에 대한 접근 방식:
   본 논문은 큐비컬 유형 이론이 book HoTT에 대해 보수적인지에 대한 열린 문제를 다루기 위한 전략을 제안한다. 2LTT 내에서 두 이론을 다음과 같이 표현함으로써:

   • Book HoTT는 MLTT + Univalence (내부 레벨)로 표현된다.
   • Cubical Type Theory는 MLMLT + Glue + Path Interval (외부/구조적 가정)로 표현된다.
     본 논문은 경로 인터벌이 있는 기저 이론 위에서, 유니밸런스 공리와 Glue 공리가 서로 유도 가능함을 증명한다. 이는 두 이론의 핵심적인 차이가 논리적이라기보다 구조적일 수 있음을 시사하며, 보수성 증명을 위한 경로를 제공한다.

의의 및 주장
본 논문은 2LTT 프레임워크가 확장 타입을 위한 "자유롭고" 균일한 토대를 제공하여, 그 규칙을 검증하기 위한 임의의 공리나 특정 모델 구성을 제거한다고 주장한다. 페이스 칼큘러스를 코피브레이션으로 내부화함으로써, 이 이론은 문헌에서 발견되는 다양한 확장 타입의 사례들을 통합한다.

큐비컬 유형 이론과 book HoTT의 관계와 관련하여, 본 논문은 신중한 입장을 취한다. 본 논문은 보수성 추측을 해결했다고 주장하는 것이 아니라, 하나의 **개념 증명(proof of concept)**을 제시한다. 즉, 2LTT의 관점에서 볼 때 큐비컬 유형 이론의 핵심 메커니즘(gluing)이 HoTT의 핵심 공리(univalence)와 논리적으로 동치임을 보여준다. 이러한 동등성은 연구자들이 구조적 확장(예: Glue 타입)을 단일 프레임워크 내에서 공리적 확장으로 번역할 수 있게 하여, 비교를 용이하게 하고 향후 보수성 증명을 위한 길을 열어준다. 본 논문은 전체적인 동치를 달anche하기 위해 HoTT 측에 "경로 인터벌"을 가정하는 것이 여전히 해결해야 할 과제로 남아 있음을 명시한다.