Univalence without function extensionality

에반 캐발로와 요나스 헤퍼의 논문 "함수 확장성 없이 동치성"에 대한 상세한 기술적 요약입니다.

1. 문제 제기

이 논문은 동치성 (Univalence, UA) 과 함수 확장성 (Function Extensionality, FE) 간의 논리적 관계에 관한 호모토피 타입 이론 (HoTT) 의 근본적인 문제를 다룹니다.

• 배경: 보에보츠키에 의한 표준 정리에 따르면, 어떤 동치성 우주 (univalent universe) 에서든 함수 확장성이 성립합니다. 즉, 두 함수가 호모토픽 ($f \sim g$) 하면 그들은 같아집니다 ($f = g$).
• 질문: 그 역은 성립할까요? 구체적으로, 두 타입의 동등성이 엄격한 역함수 (즉, 범주론적 동치) 의 존재에 대응되는 "동치성 야생 범주 (univalent wild category)"를 형성한다고 주장하는 더 약한 형태의 동치성이 함수 확장성을 함의할까요?
• 맥락: 프랑수아 G. 도레는 타입 동등성에서 범주론적 동치 (엄격한 좌우 역함수를 가진 사상) 로 가는 사상이 동치라는 **범주론적 동치성 (Categorical Univalence, CUA)**이라고 불리는 약화를 제안했습니다. 저자들은 CUA 가 FE 를 함의하는지 조사합니다.

2. 방법론

저자들은 반례를 구성하기 위해 **폰 글레인의 다항식 모델 구성 ($Poly(\mathcal{C})$)**을 사용합니다. 이 방법은 함수 확장성을 반증하는 마틴 - 뢰프 타입 이론 (ITT) 의 모델로 알려진 출처입니다.

• 기본 모델 ($\mathcal{C}$): 그들은 동치성과 함수 확장성을 만족하는 ITT 모델 (예: 큐비컬 모델) 이며 엄격한 $\eta$-규칙을 만족하는 **광범위한 유한 합 (extensive finite coproducts)**을 갖는 모델 $\mathcal{C}$로 시작합니다.
• 다항식 모델 구성: 그들은 다항식 모델 $Poly(\mathcal{C})$를 구성합니다. 이 모델에서:
  • 타입은 "형상 (shapes)"과 "위치 (positions)"를 나타내는 쌍 $(S, P)$입니다.
  • 이 구성은 괴델의 변증법 해석 (Dialectica interpretation) 과 컨테이너 범주와 관련이 있습니다.
  • 결정적으로, $Poly(\mathcal{C})$가 항상 FE 를 반증한다는 것이 알려져 있습니다.
• 동형사상 분석: 핵심 기술적 작업은 다항식 모델 내의 **동형사상 (범주론적 동치)**의 구조를 분석하는 것입니다. 저자들은 다항식 모델에서 두 타입 사이의 동형사상 타입을 다음과 같이 분해합니다:
  1. 기본 모델 $\mathcal{C}$에서의 "형상" 성분 사이의 동형사상.
  2. 형상 동형사상에 조건부로 주어진 "위치" 성분 사이의 동형사상.

3. 주요 정의 및 개념

• 야생 범주 (Wild Category): 타입의 $(\infty, 1)$-범주론적 성질을 포착하는 구조로, 여기서 합성과 항등원은 호모토피가 아닌 동등성까지 일관성 법칙을 만족합니다.
• 범주론적 동치 ($A \sim= B$): 엄격한 좌우 역함수 ($sf = id, fs = id$) 를 갖춘 사상$f: A \to B$입니다. 이는 역함수가 호모토피에서만 존재하는 *호모토피 동치* ($A \simeq B$) 와 다릅니다.
• 범주론적 동치성 (CUA): 사상 $(A = B) \to (A \sim= B)$가 동치라는 원리입니다.
• 가족적 범주론적 동치성 (CUA$^\bullet$): 임의의 인덱스 타입 $I$에 대해, $I$-인덱싱된 가족의 범주가 범주론적 의미에서 동치성을 가진다고 주장하는 더 강력한 변형입니다.
• 동치성의 분해: 논문은 표준 동치성 (UA) 이 **범주론적 동치성 (CUA)**과 **함수 확장성 (FE)**의 논리적 동치와 동등함을 확립합니다.
  $$UA \iff (CUA \land FE)$$

4. 주요 기여 및 결과

A. CUA 와 FE 의 독립성

주요 결과는 가족적 범주론적 동치성이 함수 확장성을 함의하지 않는다는 증명입니다.

• 정리: $ITT + CUA^\bullet_U \nvdash FE_U$.
• 증명 전략:
  1. $UA + FE$를 만족하는 기본 모델$\mathcal{C}$를 취합니다.
  2. $Poly(\mathcal{C})$를 구성합니다.
  3. CUA 의 보존: 저자들은 기본 모델 $\mathcal{C}$가 가족적 범주론적 동치성을 만족하면 다항식 모델 $Poly(\mathcal{C})$도 이를 만족함을 증명합니다 (정리 4.17). 이는 다항식 모델의 동형사상이 기본 모델 (형상) 의 동형사상과 기본 모델이 동치성일 때 수축 가능한 위치들에 대한 특정 조건에 의해 결정된다는 사실에 의존합니다.
  4. FE 의 반증: 다항식 모델이 함수 확장성을 반증한다는 것은 알려진 속성입니다 (명제 5.3).
  5. 결론: $Poly(\mathcal{C})$는 $ITT + CUA^\bullet_U + \neg FE_U$의 모델입니다.

B. 동치성 변형의 위계

논문은 약화된 동치성 공리들의 지형을 탐구하여 그것들이 모두 동등하지 않음을 보여줍니다:

• CUA 대 CUA$^\bullet$: 저자들은 단일 우주에 대한 CUA 가 가족적 범주론적 동치성 (CUA$^\bullet$) 을 함의하지 않음을 보입니다. 그들은 CUA 는 성립하지만 CUA$^\bullet$는 실패하는 슬라이스 모델을 구성합니다.
• 범주론적 범주론적 동치성 (CCUA): 그들은 사상 $(A=B) \to (A \sim= B)$가 호모토피 동치가 아닌 범주론적 동치인 변형을 정의합니다. 이것이 CUA 보다 엄격하게 강력하지만 여전히 FE 를 함의하지 않음을 보입니다.
• 근사적 동치성: 그들은 반 덴 베르그의 "근사적 동치성" (모든 동치성에 대한 경로의 존재) 을 논의하고, FE 와의 관계는 여전히 열린 질문이지만 다항식 모델이 관련된 "근사적 동치성 개선"을 반증한다고 지적합니다.

5. 의의

• 공리 분리: 이 논문은 우주의 "동치성" 속성이 "함수 확장성" 속성으로부터 분리될 수 있음을 보여줍니다. 이는 동치성이 모든 확장성 원리를 강제하는 단일한 공리라는 직관을 도전합니다.
• 구조적 통찰: 동치성이 범주론적 동치성과 함수 확장성으로 분해됨을 보여줌으로써, 저자들은 동치성 공리가 작동하게 만드는 요인에 대한 더 명확한 구조적 이해를 제공합니다. 이는 함수가 표준적인 동치성 진술에서 특별히 "우대"받는 이유가 FE 와의 상호작용 때문임을 시사합니다.
• 모델 이론: 이 작업은 다항식 모델 구성을 타입 이론에서 미묘한 공리들을 분리하는 강력한 도구로 검증하며, FE 반증을 넘어 동치성의 내부 구조를 분석하는 데까지 그 유용성을 확장합니다.
• 근거론적 함의: 구성주의자와 근거론 연구자들에게 이는 함수 확장성이라는 더 강력하고 역사적으로 통합하기 어려운 원리에 서약하지 않고도 타입의 구조적 동치성을 보존하는 동치성 형태 (범주론적 동치성) 를 채택할 수 있음을 시사합니다.

요약하자면, 이 논문은 도레의 질문에 부정적으로 답합니다: 범주론적 동치성은 완전한 동치성보다 엄격하게 약하며 함수 확장성을 함의하지 않습니다.