이중 레벨 타입 이론

이중 레벨 타입 이론 (Two-Level Type Theory)

기초 (Basics)

이중 레벨 타입 이론(Two-level type theory, 2LTT)은 두 타입 이론을 결합한 Martin-Löf 타입 이론의 버전을 가리켜요: 하나는 잠재적으로 호모토피 타입 이론이거나 큐빅 타입 이론일 수 있는 "내부" 레벨로, 유니벌런트 유니버스와 높은 귀납 타입을 포함할 수 있고, 다른 하나는 동일성 증명의 유일성(uniqueness of identity proofs)을 검증하는 두 번째 "외부" 레벨이에요.

Agda는 버전 2.6.2부터 --two-level 플래그로 2LTT를 활성화해요.

두 레벨은 두 개의 유니버스 계층으로 구분돼요: 내부 레벨을 위한 평소의 유니버스 Set과, 외부 레벨을 위한 "엄격 집합(strict sets)"을 뜻하는 SSet으로 표기되는 새로운 유니버스 계층이에요.

참고: SSet의 타입들은 문헌에서 다양한 이름으로 불려요. 이들은 HTS (2017)에서 비-섬유 타입(non-fibrant types), 2LTT (2017)에서 외부 타입(outer types), UP (2021)에서 엑소 타입(exo-types)이라 불려요. 마찬가지로, 이 참고 문헌들은 Set의 타입을 각각 섬유 타입(fibrant types), 내부 타입, 타입이라고 부르며, 이 문서에서도 같은 용어를 사용해요.

함수 타입은 도메인과 코도메인이 모두 Set에 속하면 Set에 속하고, 그렇지 않으면 SSet에 속해요. 레코드와 데이터 타입은 항상 SSet에 속하도록 선언할 수 있고, 모든 입력이 Set에 속하면 대신 Set에 속하도록 선언할 수도 있어요. 특히 Set의 임의의 타입은 자명한 레코드를 사용해 SSet으로 올릴 수 있어요:

record c (A : Set) : SSet where
  constructor ↑
  field
    ↓ : A

open c

두 레벨의 주요 차이점은, 첫째로 --without-K와 --cubical 같은 호모토피 플래그가 Set 레벨에만 적용된다는 점(SSet 레벨은 결코 호모토피적이지 않음)이고, 둘째로 내부 레벨에 속하는 데이터 타입은 motive가 외부 레벨에 속할 때 패턴 매칭할 수 없다는 점이에요 (이전 구분을 유지하는 데 필요해요).

주요 예로, 두 레벨 각각에 대해 별도의 귀납 동일성 타입을 정의할 수 있어요:

infix 4 _≡ˢ_ _≡_

data _≡ˢ_ {a} {A : SSet a} (x : A) : A → SSet a where
  reflˢ : x ≡ˢ x

data _≡_ {a} {A : Set a} (x : A) : A → Set a where
  refl : x ≡ x

이 정의들로 --without-K나 --cubical이 활성화되어 있어도 엄격 동일성에 대한 동일성 증명의 유일성을 증명할 수 있어요:

UIP : {a : Level} {A : SSet a} {x y : A} (p q : x ≡ˢ y) → p ≡ˢ q
UIP reflˢ reflˢ = reflˢ

또한 엄격하게 같은 원소는 비-엄격하게도 같다는 것을 증명할 수 있어요:

≡ˢ-to-≡ : {A : Set} {x y : c A} → (x ≡ˢ y) → (↓ x ≡ ↓ y)
≡ˢ-to-≡ reflˢ = refl

하지만 반대 함의는 실패해요. 앞서 말했듯 motive가 SSet에 있을 때 Set의 데이터 타입에 대해 패턴 매칭할 수 없기 때문이에요. 비슷하게 엄격한 자연수를 보통 자연수로 매핑할 수 있어요:

data ℕ : Set where
  zero : ℕ
  succ : ℕ → ℕ

data ℕˢ : SSet where
  zeroˢ : ℕˢ
  succˢ : ℕˢ → ℕˢ

ℕˢ-to-ℕ : ℕˢ → ℕ
ℕˢ-to-ℕ zeroˢ = zero
ℕˢ-to-ℕ (succˢ n) = succ (ℕˢ-to-ℕ n)

하지만 그 반대는 안 돼요.

(Agda는 현재 빈 SSet에서 빈 Set으로의 매핑은 허용하지만, 이 기능은 논쟁 중이에요.)

--two-level 플래그를 --cumulativity와 결합하면 각 유니버스 Set a가 SSet a의 부분 타입이 돼요. 이 경우 변환 c를 항등 함수로 정의할 수 있어요:

c' : Set → SSet
c' A = A

그리고 변환 ↑와 ↓를 항등 함수로 대체할 수 있어요. 하지만 이 조합은 현재 허용되지 않아야 할 일부 함수를 정의할 수 있게 해요. 자세한 내용은 Agda 이슈 #5761을 참고하세요.

더 알아보기 (Learn more)