큐빅

큐빅 (Cubical)

큐빅 모드는 큐빅 타입 이론(Cubical Type Theory)의 다양한 기능으로 Agda를 확장해요.

특히 계산적 유니발런스(computational univalence)와 고차 귀납 타입(higher inductive types)을 추가해서, 호모토피 타입 이론(Homotopy Type Theory)과 유니발런트 기초(Univalent Foundations)에 계산적 의미를 부여해요. Agda가 구현하는 큐빅 타입 이론의 버전은 Kan 합성 연산이 동질 합성(homogeneous composition)과 일반화된 transport로 분해되는 CCHM 큐빅 타입 이론의 변형이에요. 이것이 CHM 논문을 따라 고차 귀납 타입의 일반적인 스키마가 작동하게 만드는 것이에요. Cubical Agda에 대해 구체적으로 다룬 연구 논문도 https://www.doi.org/10.1017/S0956796821000034 에 있어요.

큐빅 모드를 사용하려면 Agda를 --cubical 명령줄 옵션으로 실행하거나, .agda-lib 파일에 플래그로 넣거나, 파일 맨 위에 {-# OPTIONS --cubical #-}로 넣어야 해요.

큐빅 모드에는 두 가지 다른 변형도 있어요:

--cubical=erased — 아래에 설명.
--cubical=no-glue — Glue 타입 없이 Cubical 기능을 허용. 아래에 설명.

큐빅 모드는 Agda에 다음 기능들을 추가해요:

구간 타입과 경로 타입
일반화된 transport (transp)
부분 원소 (Partial elements)
동질 합성 (hcomp)
Glue 타입
고차 귀납 타입
큐빅 항등 타입

이 문서에서는 https://github.com/agda/cubical 에 있는 agda/cubical 라이브러리에 의존할 거예요. 우리는 이 라이브러리의 명명 규칙을 사용해요; 모든 내장된 Cubical Agda 파일과 프리미티브의 상세 목록은 부록: Cubical Agda 프리미티브를 참고하세요.

큐빅 프리미티브에 접근하기 위한 권장 방법은 파일 맨 위에 다음을 추가하는 것이에요; 이것은 agda/cubical 라이브러리가 설치되어 Agda에 보임을 가정해요.

{-# OPTIONS --cubical #-}

open import Cubical.Core.Primitives
open import Cubical.Core.Glue

라이브러리를 설치하려면 https://github.com/agda/cubical 의 지침을 따르세요. 이 라이브러리를 Agda에 보이게 하려면 /path/to/cubical/cubical.agda-lib을 .agda/libraries에, cubical을 .agda/defaults에 추가하세요 (여기서 path/to는 agda/cubical 라이브러리가 설치된 절대 경로). Agda의 라이브러리 관리에 대한 자세한 내용은 라이브러리 관리(Library Management)를 참고하세요.

agda/cubical에 의존하고 싶지 않은 고급 사용자는 관련 import 문을 파일 맨 위에 추가하면 됩니다 (자세한 내용은 부록: Cubical Agda 프리미티브 참고). 하지만 초보자는 agda/cubical 라이브러리의 핵심 부분을 적어도 사용하는 것이 권장돼요.

구간과 경로 타입 (The interval and path types)

큐빅 타입 이론의 핵심 아이디어는 구간 타입 I : IUniv를 추가하는 것이에요 (이것이 특수 소트 IUniv에 있는 이유는 transp와 hcomp 연산을 지원하지 않기 때문이에요). 변수 i : I는 직관적으로 실수 단위 구간의 점에 대응해요. 빈 문맥에는 타입 I의 값이 두 개만 있어요: 구간의 두 끝점 i0과 i1.

i0 : I
i1 : I

구간의 원소들은 최소(∧), 최대(∨), 부정(~)을 가진 De Morgan 대수를 형성해요.

_∧_ : I → I → I
_∨_ : I → I → I
~_ : I → I

De Morgan 대수의 모든 속성이 정의적으로 성립해요. 구간의 끝점 i0과 i1은 각각 바닥(bottom)과 꼭대기(top) 원소예요.

i0 ∨ i    = i
i1 ∨ i    = i1
i  ∨ j    = j ∨ i
i0 ∧ i    = i0
i1 ∧ i    = i
i  ∧ j    = j ∧ i
~ (~ i)   = i
i0        = ~ i1
~ (i ∨ j) = ~ i ∧ ~ j
~ (i ∧ j) = ~ i ∨ ~ j

호모토피 타입 이론과 유니발런트 기초의 핵심 아이디어는 경로(위상수학에서)와 (증명-관련) 동등성(Martin-Löf의 항등 타입에서) 사이의 대응이에요. 이 대응은 Cubical Agda에서 매우 문자 그대로 받아들여지는데, 타입 A의 경로는 함수 I → A처럼 구간 밖의 함수로 표현돼요. 경로 타입은 사실 더 일반적인 내장의 이종 경로 타입(heterogeneous path types)의 특수한 경우예요:

-- PathP : ∀ {ℓ} (A : I → Set ℓ) → A i0 → A i1 → Set ℓ

-- 비의존 경로 타입
Path : ∀ {ℓ} (A : Set ℓ) → A → A → Set ℓ
Path A a b = PathP (λ _ → A) a b

Cubical Agda에서 동등성의 중심 개념은 따라서 이종 동등성(HoTT의 PathOver 의미에서)이에요. 경로를 정의하려면 λ-추상화를 사용하고, 적용하려면 일반 적용을 사용해요. 예를 들어 이것은 상수 경로(또는 반사성 증명)의 정의예요:

refl : ∀ {ℓ} {A : Set ℓ} {x : A} → Path A x x
refl {x = x} = λ i → x

같은 문법을 사용하지만 경로는 함수와 정확히 같지는 않아요. 예를 들어 타입된 람다는 경로를 형성하는 데 사용될 수 없고, 함수용으로 예약돼 있어요:

not-refl : ∀ {ℓ} {A : Set ℓ} {x : A} → (i : I) → A
not-refl {x = x} = λ (i : I) → x

경로가 동등성에 대응한다는 직관 때문에 PathP (λ i → A) x y는 A가 i를 언급하지 않을 때 x ≡ y로 출력돼요. 경로 타입을 반복함으로써 Agda에서 정사각형, 입방체, 더 높은 입방체를 정의할 수 있어 타입 이론을 큐빅으로 만들어요. 예를 들어 A의 정사각형은 4개의 점과 4개의 선으로 만들어져요:

Square : ∀ {ℓ} {A : Set ℓ} {x0 x1 y0 y1 : A} →
           x0 ≡ x1 → y0 ≡ y1 → x0 ≡ y0 → x1 ≡ y1 → Set ℓ
Square p q r s = PathP (λ i → p i ≡ q i) r s

동등성을 구간 밖의 함수로 보는 것은 동등성 추론을 매우 직접적인 방식으로 많이 할 수 있게 해줘요:

sym : ∀ {ℓ} {A : Set ℓ} {x y : A} → x ≡ y → y ≡ x
sym p = λ i → p (~ i)

cong : ∀ {ℓ} {A : Set ℓ} {x y : A} {B : A → Set ℓ} (f : (a : A) → B a) (p : x ≡ y)
       → PathP (λ i → B (p i)) (f x) (f y)
cong f p i = f (p i)

함수가 계산하는 방식 때문에 이것들은 표준 Agda 정의에 비해 몇 가지 새로운 정의적 동등성을 만족해요:

symInv : ∀ {ℓ} {A : Set ℓ} {x y : A} (p : x ≡ y) → sym (sym p) ≡ p
symInv p = refl

congId : ∀ {ℓ} {A : Set ℓ} {x y : A} (p : x ≡ y) → cong (λ a → a) p ≡ p
congId p = refl

congComp : ∀ {ℓ} {A B C : Set ℓ} (f : A → B) (g : B → C) {x y : A} (p : x ≡ y) →
             cong (λ a → g (f a)) p ≡ cong g (cong f p)
congComp f g p = refl

경로 타입은 또한 표준 Agda에서 증명할 수 없는 새로운 것들을 증명하게 해줘요. 예를 들어 점별로 같은 함수는 같다는 함수 외연성(function extensionality)은 매우 간단한 증명을 가져요:

funExt : ∀ {ℓ} {A : Set ℓ} {B : A → Set ℓ} {f g : (x : A) → B x} →
           ((x : A) → f x ≡ g x) → f ≡ g
funExt p i x = p x i

Transport

경로 타입은 동등성 추론에 훌륭하지만, 타입 사이의 경로를 따라 transport하거나 경로조차 합성하게 해주지 않아서, 특히 경로에 대한 귀납 원리를 아직 증명할 수 없음을 의미해요. 해결책으로 내장된 (일반화된) transport 연산 transp와 동질 합성 연산 hcomp가 있어요.

transport 연산은 그것이 항등 함수인 곳을 지정할 수 있게 해준다는 의미에서 일반화돼요.

transp : ∀ {ℓ} (A : I → Set ℓ) (r : I) (a : A i0) → A i1

transp의 사용이 타입 체크되기 위해 만족되어야 하는 추가 부수 조건이 있어요: 제약 r = i1이 만족될 때마다 A는 상수 함수여야 해요. 여기서 상수란 A가 λ _ → A i0와 정의적으로 같다는 뜻이며, 이는 차례로 A i0와 A i1도 정의적으로 같아야 함을 요구해요.

r이 i1이면 transp A r는 항등 함수로 계산돼요.

transp A i1 a = a

이것은 그러한 경우에 A가 사소한 경로인 경우에만 건전한데, 부수 조건이 요구하듯이요.

부수 조건이 r과 A가 상호작용할 것을 기대하는 것이 이상해 보일 수 있지만, 둘 다 스코프의 임의의 구간 변수에 의존할 수 있으므로 r의 특정 값을 가정하는 것이 A가 어떻게 보이는지에 영향을 줄 수 있어요.

다른 r 값에 대한 부수 조건의 몇 가지 예:

r이 스코프의 어떤 변수 i이고 A도 그에 의존할 수 있으면, A는 i에 i1을 대입할 때만 상수 함수일 필요가 있어요.
r이 i0이면 A에 제한이 없어요. 부수 조건이 공허하게 참이기 때문이에요.
r이 i1이면 A는 상수 함수여야 해요.

transp로 일반 transport를 정의할 수 있어요:

transport : ∀ {ℓ} {A B : Set ℓ} → A ≡ B → A → B
transport p a = transp (λ i → p i) i0 a

transport와 최소 연산을 결합하면 경로에 대한 귀납 원리를 정의할 수 있어요:

J : ∀ {ℓ} {A : Set ℓ} {x : A} (P : ∀ y → x ≡ y → Set ℓ)
      (d : P x refl) {y : A} (p : x ≡ y)
    → P y p
J P d p = transport (λ i → P (p i) (λ j → p (i ∧ j))) d

경로와 Agda의 명제적 동등성 타입 사이의 미묘한 차이 하나는 J의 계산 규칙이 정의적으로 성립하지 않는다는 것이에요. J가 Agda 표준 라이브러리처럼 패턴 매칭으로 정의되면 이것이 성립하지만, 경로 타입은 귀납적으로 정의되지 않으므로 위 J 정의에는 성립하지 않아요. 특히 상수 족에서의 transport는 경로까지의 항등 함수일 뿐이라서 J의 계산 규칙은 경로까지만 성립해요:

transportRefl : ∀ {ℓ} {A : Set ℓ} (x : A) → transport refl x ≡ x
transportRefl {A = A} x i = transp (λ _ → A) i x

JRefl : ∀ {ℓ} {A : Set ℓ} {x : A} (P : ∀ y → x ≡ y → Set ℓ)
         (d : P x refl) → J P d refl ≡ d
JRefl P d = transportRefl d

Agda 내부에서 transp 연산은 타입에 따라 경우를 나누며 계산하는데, 예를 들어 Σ-타입의 경우 원소별로 계산돼요. 하지만 경로 타입의 경우 transport 후에 경로의 끝점을 기억할 방법이 필요하므로 아직 계산 규칙을 제공할 수 없어요. 게다가 이것은 임의의 고차원 입방체에 대해 동작해야 해요 (경로 타입을 반복할 수 있으므로). 이를 위해 "동질 합성 연산"(hcomp)을 도입하는데, 이것은 경로의 이항 합성을 고차원 입방체의 n-항 합성으로 일반화해요.

부분 원소 (Partial elements)

동질 합성 연산을 설명하려면 부분적으로 지정된 n차원 입방체(즉 일부 면이 빠진 입방체)를 쓸 수 있어야 해요. 구간 r : I의 원소가 주어지면 제약 r = i1을 나타내는 술어 IsOne이 있어요. 이것은 i1이 실제로 i1과 같다는 증명 1=1 : IsOne i1을 동반해요. 그러한 r이 IsOne의 정의역에 있는 것으로 생각되어야 할 때 φ나 ψ 같은 그리스 문자를 사용해요.

이것으로 Partial φ A라고 불리는 부분 원소의 타입을 도입해요. 아이디어는 Partial φ A가 IsOne φ가 성립할 때만 정의되는 A의 입방체의 타입이라는 것이에요.

Partial φ A는 더 외연적인 판단적 동등성을 가진 IsOne φ → A의 특수 버전이에요: Partial φ A의 두 원소는 그것들이 같은 부분 입방체를 나타내면 같다고 간주돼요; 그래서 입방체의 면이 예를 들어 다른 순서로 주어질 수 있어도 두 원소는 여전히 같다고 간주돼요.

A가 IsOne φ일 때만 정의되도록 요구하는 Partial φ A의 의존 버전인 PartialP φ A도 있어요.

Partial : ∀ {ℓ} → I → Set ℓ → SSet ℓ

PartialP : ∀ {ℓ} → (φ : I) → Partial φ (Set ℓ) → SSet ℓ

부분 원소를 도입하는 데 사용할 수 있는 새 형태의 패턴 매칭이 있어요:

partialBool : ∀ i → Partial (i ∨ ~ i) Bool
partialBool i (i = i0) = true
partialBool i (i = i1) = false

항 partialBool i는 (i = i0)과 (i = i1)에서 다른 값을 가진 불리언으로 생각해야 해요. 타입 Partial φ A의 항은 패턴 람다를 사용해 도입할 수도 있어요.

partialBool' : ∀ i → Partial (i ∨ ~ i) Bool
partialBool' i = λ where
  (i = i0) → true
  (i = i1) → false

경우가 겹치면 일치해야 해요:

partialBool'' : ∀ i j → Partial (~ i ∨ i ∨ (i ∧ j)) Bool
partialBool'' i j = λ where
  (i = i1)          → true
  (i = i1) (j = i1) → true
  (i = i0)          → false

경우의 순서가 구간 공식과 정확히 일치할 필요는 없다는 점에 유의하세요. 게다가 IsOne i0은 실제로 부정(불가능)이에요:

empty : {A : Set} → Partial i0 A
empty = λ()

Cubical Agda는 CCHM 타입 이론처럼 큐빅 부분타입(subtypes)도 가져요:

_[_↦_] : ∀ {ℓ} (A : Set ℓ) (φ : I) (u : Partial φ A) → SSet ℓ
A [ φ ↦ u ] = Sub A φ u

항 v : A [ φ ↦ u ]는 IsOne φ가 만족될 때 정의적으로 u : A와 같은 타입 A의 항으로 생각해야 해요. 임의의 항 u : A는 φ에서 자기 자신과 일치하는 A [ φ ↦ u ]의 항으로 볼 수 있어요:

inS : ∀ {ℓ} {A : Set ℓ} {φ : I} (u : A) → A [ φ ↦ (λ _ → u) ]

부분 원소가 u와 φ에서 일치한다는 것을 잊을 수도 있어요:

outS : ∀ {ℓ} {A : Set ℓ} {φ : I} {u : Partial φ A} → A [ φ ↦ u ] → A

이 강제들은 다음 동등성을 만족해요:

outS (inS a) = a

inS {φ = φ} (outS {φ = φ} a) = a

outS {φ = i1} {u} _ = u 1=1

a : A [ φ ↦ u ]와 α : IsOne φ가 주어졌을 때 outS a = u α는 성립하지 않지만, 패턴 바인딩 (φ = i1) 아래에서는 outS a = u 1=1이 성립한다는 점에 유의하세요.

이 모든 큐빅 인프라로 이제 hcomp 연산을 설명할 수 있어요.

동질 합성 (Homogeneous composition)

동질 합성 연산은 여러 개의 합성 가능한 입방체를 합성할 수 있도록 경로의 이항 합성을 일반화해요.

hcomp : ∀ {ℓ} {A : Set ℓ} {φ : I} (u : I → Partial φ A) (u0 : A) → A

hcomp {φ = φ} u u0를 호출할 때 Agda는 u0이 φ에서 u i0과 일치하는지 확인해요. 아이디어는 u0이 밑면이고 u가 열린 상자의 옆면들을 지정한다는 것이에요. 이것은 따라서 u0의 반대쪽 면이 없는 열린 (고차원) 입방체예요. 그러면 hcomp 연산은 u0의 반대쪽에 있는 빠진 면을 주어요. 예를 들어 경로의 이항 합성은 다음과 같이 쓸 수 있어요:

compPath : ∀ {ℓ} {A : Set ℓ} {x y z : A} → x ≡ y → y ≡ z → x ≡ z
compPath {x = x} p q i = hcomp (λ{ j (i = i0) → x
                                 ; j (i = i1) → q j })
                               (p i)

도식적으로 p : x ≡ y와 q : y ≡ z가 주어지고, 두 경로의 합성은 이 열린 정사각형의 빠진 뚜껑을 계산하여 얻어져요:

x             z
  ^             ^
  |             |
x |             | q j
  |             |
  x ----------> y
       p i

그림에서 방향 i는 왼쪽에서 오른쪽으로, j는 아래에서 위로 가요. i를 따라 x에서 z로의 경로를 만들므로 문맥에 이미 i : I가 있고 밑면에 p i를 넣어요. 합성을 하는 방향 j는 hcomp의 첫 번째 인자에서 추상화돼요.

부분 원소 u가 열린 상자의 모든 옆면을 지정할 필요는 없다는 점에 유의하세요; 더 많은 옆면을 주는 것은 단순히 hcomp 결과에 대한 더 많은 제어를 줘요.

예를 들어 compPath 정의에서 (i = i0) → x 옆면을 생략하면 여전히 타입 A의 유효한 항을 얻어요. 하지만 그 항은 i = i0일 때 hcomp (λ{ j () }) x로 축약되어서, 그 정의는 x에서 시작하는 경로를 만들지 않을 거예요.

입방체의 동질 채움(homogeneous filling)도 정의할 수 있어요:

hfill : ∀ {ℓ} {A : Set ℓ} {φ : I}
        (u : ∀ i → Partial φ A) (u0 : A [ φ ↦ u i0 ])
        (i : I) → A
hfill {φ = φ} u u0 i = hcomp (λ{ j (φ = i1) → u (i ∧ j) 1=1
                               ; j (i = i0) → outS u0 })
                             (outS u0)

i가 i0이면 이것은 u0이고 i가 i1이면 hcomp u u0이에요. 따라서 열린 상자의 내부를 주는 것으로 볼 수 있어요. 위 정사각형의 특수한 경우에서 hfill은 p를 refl과 합성하는 것이 p라는 직접적인 큐빅 증명을 주어요.

compPathRefl : ∀ {ℓ} {A : Set ℓ} {x y : A} (p : x ≡ y) → compPath p refl ≡ p
compPathRefl {x = x} {y = y} p j i = hfill (λ{ _ (i = i0) → x
                                             ; _ (i = i1) → y })
                                           (inS (p i))
                                           (~ j)

Glue 타입 (Glue types)

유니발런스 정리를 증명할 수 있으려면 "Glue" 타입도 추가해야 해요. 이것들은 타입 사이의 동치를 타입 사이의 경로로 바꿀 수 있게 해줘요. 타입 A와 B의 동치는 그 올(fibers)이 수축 가능한(contractible) 사상 f : A → B로 정의돼요.

fiber : ∀ {ℓ} {A B : Set ℓ} (f : A → B) (y : B) → Set ℓ
fiber {A = A} f y = Σ[ x ∈ A ] f x ≡ y

isContr : ∀ {ℓ} → Set ℓ → Set ℓ
isContr A = Σ[ x ∈ A ] (∀ y → x ≡ y)

record isEquiv {ℓ} {A B : Set ℓ} (f : A → B) : Set ℓ where
  field
    equiv-proof : (y : B) → isContr (fiber f y)

_≃_ : ∀ {ℓ} (A B : Set ℓ) → Set ℓ
A ≃ B = Σ[ f ∈ (A → B) ] (isEquiv f)

동치의 가장 간단한 예는 항등 함수예요.

idfun : ∀ {ℓ} → (A : Set ℓ) → A → A
idfun _ x = x

idIsEquiv : ∀ {ℓ} (A : Set ℓ) → isEquiv (idfun A)
equiv-proof (idIsEquiv A) y =
  ((y , refl) , λ z i → z .snd (~ i) , λ j → z .snd (~ i ∨ j))

idEquiv : ∀ {ℓ} (A : Set ℓ) → A ≃ A
idEquiv A = (idfun A , idIsEquiv A)

동치 타입의 중요한 특수한 경우는 동형(isomorphic) 타입(즉 서로 역인 앞뒤로 가는 사상이 있는 타입)이에요.

모든 것이 고차원까지 동작해야 하므로 Glue 타입은 기본 타입 A와 동치인 타입의 부분 족을 취해요:

Glue : ∀ {ℓ ℓ'} (A : Set ℓ) {φ : I}
     → Partial φ (Σ[ T ∈ Set ℓ' ] T ≃ A) → Set ℓ'

이것들은 생성자와 제거자를 동반해요:

glue : ∀ {ℓ ℓ'} {A : Set ℓ} {φ : I} {Te : Partial φ (Σ[ T ∈ Set ℓ' ] T ≃ A)}
     → PartialP φ T → A → Glue A Te

unglue : ∀ {ℓ ℓ'} {A : Set ℓ} (φ : I) {Te : Partial φ (Σ[ T ∈ Set ℓ' ] T ≃ A)}
       → Glue A Te → A

Glue 타입을 사용해 타입의 동치를 다음과 같이 경로로 바꿀 수 있어요:

ua : ∀ {ℓ} {A B : Set ℓ} → A ≃ B → A ≡ B
ua {_} {A} {B} e i = Glue B λ{ (i = i0) → (A , e)
                             ; (i = i1) → (B , idEquiv B) }

아이디어는 i = i0일 때 e를 사용해 A를 B와 붙이고(glue), i = i1일 때 항등 동치를 사용해 B를 자기 자신과 붙이는 것이에요. 이것이 유니발런스의 핵심 부분, 즉 동치를 경로로 바꾸는 함수를 주어요. 유니발런스의 다른 부분은 이 사상 자체가 동치라는 것인데, 이것은 ua의 계산 규칙에서 따라와요:

uaβ : ∀ {ℓ} {A B : Set ℓ} (e : A ≃ B) (x : A) → transport (ua e) x ≡ e .fst x
uaβ e x = transportRefl (e .fst x)

동치에 ua를 적용해 얻은 경로를 따라 transport하는 것은 동치를 적용하는 것과 같아요. 이것이 Cubical Agda에서 유니발런스 공리를 계산적으로 사용할 수 있게 하는 것이에요: 우리는 동치를 경로로 묶고, 이 경로들로 동등성 추론을 하고, 마지막에는 경로를 따라 transport하여 동치로 계산할 수 있어요.

우리는 다음 동등성을 가져요:

Glue A {i1} Te = Te 1=1 .fst

unglue φ (glue t a) = a

glue (λ{ (φ = i1) → g }) (unglue φ g) = g

unglue i1 {Te} g = Te 1=1 .snd .fst g

glue {φ = i1} t a = t 1=1

Glue 타입과 유니발런스에 대한 더 많은 결과는 agda/cubical 라이브러리의 Glue 타입과 유니발런스 파일을 참고하세요.

고차 귀납 타입 (Higher inductive types)

Cubical Agda는 또한 고차 귀납 타입을 경로 생성자를 가진 데이터 타입으로 직접 정의할 수 있게 해줘요. 예를 들어 원(circle)과 토러스(torus)는 다음과 같이 정의할 수 있어요:

data S¹ : Set where
  base : S¹
  loop : base ≡ base

data Torus : Set where
  point : Torus
  line1 : point ≡ point
  line2 : point ≡ point
  square : PathP (λ i → line1 i ≡ line1 i) line2 line2

고차 귀납 타입 밖의 함수는 그런 다음 패턴 매칭으로 정의할 수 있어요:

t2c : Torus → S¹ × S¹
t2c point        = (base   , base)
t2c (line1 i)    = (loop i , base)
t2c (line2 j)    = (base   , loop j)
t2c (square i j) = (loop i , loop j)

c2t : S¹ × S¹ → Torus
c2t (base   , base)   = point
c2t (loop i , base)   = line1 i
c2t (base   , loop j) = line2 j
c2t (loop i , loop j) = square i j

경로와 정사각형 생성자의 경우를 줄 때 함수가 경계를 올바른 것에 매핑하는지 확인해야 해요. 예를 들어 다음 정의는 마지막 경우의 경계가 정사각형 생성자의 기대 경계와 일치하지 않으므로(line1과 line2 경우가 뒤섞여 있으므로) Agda의 타입 체커를 통과하지 못해요.

c2t_bad : S¹ × S¹ → Torus
c2t_bad (base   , base)   = point
c2t_bad (loop i , base)   = line2 i
c2t_bad (base   , loop j) = line1 j
c2t_bad (loop i , loop j) = square i j

고차 귀납 타입에 대한 패턴 매칭으로 정의된 함수는 모든 생성자에 대해 정의적으로 계산돼요.

c2t-t2c : ∀ (t : Torus) → c2t (t2c t) ≡ t
c2t-t2c point        = refl
c2t-t2c (line1 _)    = refl
c2t-t2c (line2 _)    = refl
c2t-t2c (square _ _) = refl

t2c-c2t : ∀ (p : S¹ × S¹) → t2c (c2t p) ≡ p
t2c-c2t (base   , base)   = refl
t2c-c2t (base   , loop _) = refl
t2c-c2t (loop _ , base)   = refl
t2c-c2t (loop _ , loop _) = refl

이 동형을 동치로 바꾸면 토러스가 두 원과 같다는 직접적인 증명을 얻어요.

Torus≡S¹×S¹ : Torus ≡ S¹ × S¹
Torus≡S¹×S¹ = isoToPath (iso t2c c2t t2c-c2t c2t-t2c)

타입은 모든 원소가 경로로 연결되면 명제(proposition)예요:

IsProp : ∀ {ℓ} → Set ℓ → Set ℓ
IsProp A = (x y : A) → x ≡ y

Cubical Agda는 매개변수화되고 재귀적인 고차 귀납 타입도 지원해요. 예를 들어 명제 절단(propositional truncation, squash 타입)은 다음과 같이 정의돼요:

data ∥_∥ {ℓ} (A : Set ℓ) : Set ℓ where
  ∣_∣ : A → ∥ A ∥
  squash : ∀ (x y : ∥ A ∥) → x ≡ y

recPropTrunc : ∀ {ℓ} {A : Set ℓ} {P : Set ℓ} → IsProp P → (A → P) → ∥ A ∥ → P
recPropTrunc Pprop f ∣ x ∣          = f x
recPropTrunc Pprop f (squash x y i) =
  Pprop (recPropTrunc Pprop f x) (recPropTrunc Pprop f y) i

소거된 생성자 (Erased constructors)

--erasure와 결합하면 생성자, 특히 squash 같은 고차 생성자를 소거로 표시하는 것이 말이 될 수 있어요:

data ∥_∥ {ℓ} (A : Set ℓ) : Set ℓ where
  ∣_∣ : A → ∥ A ∥
  @0 squash : ∀ (x y : ∥ A ∥) → x ≡ y

recPropTrunc : ∀ {ℓ} {A : Set ℓ} {P : Set ℓ} → @0 IsProp P → (A → P) → ∥ A ∥ → P
recPropTrunc Pprop f ∣ x ∣          = f x
recPropTrunc Pprop f (squash x y i) =
  Pprop (recPropTrunc Pprop f x) (recPropTrunc Pprop f y) i

위 코드에서 생성자 squash는 컴파일 타임에만 사용 가능하고, ∣_∣는 런타임에도 사용 가능해요. 비-소거 위치에서 소거된 생성자에 매칭하는 절은 (적어도 일부) 컴파일러 백엔드에 의해 생략되므로 그러한 절의 본문에서 소거된 이름을 사용할 수 있어요. (원래 소거로 선언되지 않았지만 현재 소거된 것으로 취급되는 생성자에 대한 예외가 있어요.)

고차 귀납 타입의 더 많은 예는 agda/cubical 라이브러리를 참고하세요.

인덱스된 귀납 타입 (Indexed inductive types)

Cubical Agda는 인덱스된 귀납 타입의 인덱스를 치환하는 데 transp 프리미티브를 사용하는 실험적 지원을 가져요. 소수의 정의(패턴 매칭에 대한 기술적 제한을 만족하는)는 인덱스를 따라 transport에 적용될 때 계산돼요. 작동하는 예로 다음 실행 예제를 생각해 봐요:

data Eq {a} {A : Set a} (x : A) : A → Set a where
  reflEq : Eq x x

data Vec {a} (A : Set a) : Nat → Set a where
  []  : Vec A zero
  _∷_ : ∀ {n} → A → Vec A n → Vec A (suc n)

Eq의 모든 끝점이 변수일 때 Eq에 매칭하는 함수들, 즉 아래 symEq와 transpEq 같은 매우 일반적인 보조정리는 모든 경우에 계산해요: 그것들은 인자가 reflEq일 때 주어진 오른쪽 변으로 정의적으로 계산하고, 인자가 두 번째 변수에서 transport되었을 때는 공역에서의 transport로 계산해요.

symEq : ∀ {a} {A : Set a} {x y : A} → Eq x y → Eq y x
symEq reflEq = reflEq

transpEq : ∀ {a} {A B : Set a} → Eq A B → A → B
transpEq reflEq x = x

pathToEq : ∀ {a} {A : Set a} {x y : A} → x ≡ y → Eq x y
pathToEq {x = x} p = transp (λ i → Eq x (p i)) i0 reflEq

module _ {a} {A B : Set a} {x y : A} {f : A ≃ B} where
  _ : symEq (reflEq {x = x}) ≡ reflEq
  _ = refl

  _ : transpEq (pathToEq (ua (idEquiv Bool))) ≡ λ x → x
  _ = refl

타입이 가정되는(따라서 그 transport도 열려 있는) 상황에서 인덱스된 타입에 매칭하는 것은 경로가 있는 비교 가능한 구성보다 훨씬 많은 transport를 생성하는 경우가 많아요. 예를 들어 아래 uaβEq의 증명에는 네 개의 보류된 transport가 있는 반면, uaβ에는 하나만 있어요!

uaβEq : transpEq (pathToEq (ua f)) ≡ f .fst
uaβEq = funExt λ z →
  compPath (transportRefl (f .fst _))
    (cong (f .fst) (compPath
      (transportRefl _)
      (compPath
        (transportRefl _)
        (transportRefl _))))

인덱스가 어떤 다른 귀납 타입의 생성자 같은 더 구체적인 상황에서는 패턴 매칭 정의가 transport에 적용될 때 계산하지 않아요. 특정 비지원 경우에 대해서는 무엇이 작동하고 무엇이 작동하지 않는지(What works, and what doesn't)를 참고하세요.

UnsupportedIndexedMatch 경고가 활성화되면(기본적으로 활성) Agda는 계산적 동작이 transport를 포괄하도록 확장될 수 없었던 모든 정의에 대해 경고를 출력해요. 내부적으로 transport는 추가 생성자로 표현되며, 패턴 매칭 정의는 이 생성자들을 포괄하도록 확장되어야 해요. 이를 위해 패턴 매칭 통일의 결과가 (HoTT 의미의) 매립(embedding)으로 번역되어야 해요. 이것은 진행 중인 작업이에요.

Cubical Agda의 일상적 사용에서는 UnsupportedIndexedMatch 경고를 비활성화하는 것이 좋아요. OPTIONS 프래그마나 agda-lib 파일에서 -WnoUnsupportedIndexedMatch 옵션으로 할 수 있어요.

무엇이 작동하고 무엇이 작동하지 않는지 (What works, and what doesn't)

이 섹션은 패턴 매칭 통일이 transport를 포괄하도록 확장될 수 없는 흔한 경우들과, 확장될 수 있는 경우들 중 일부를 나열해요.

다음 정의 쌍은 데이터 생성자(특히 생성자 suc)의 단사성에 의존하므로 transport된 값에 대해 계산하지 않을 거예요.

sucInjEq : ∀ {n k} → Eq (suc n) (suc k) → Eq n k
sucInjEq reflEq = reflEq

head : ∀ {n} {a} {A : Set a} → Vec A (suc n) → A
head (x ∷ _) = x

계산 실패를 보여주기 위해 head를 사용하는 다음 인위적 예를 설정할 수 있어요. 벡터 true ∷ []를 두 개의 transport(취소될지라도)로 통과시키면 head의 계산이 멈춰요.

module _ (n : Nat) (p : n ≡ 1) where private
  vec : Vec Bool n
  vec = transport (λ i → Vec Bool (p (~ i))) (true ∷ [])

  hd : Bool
  hd = head (transport (λ i → Vec Bool (p i)) vec)

-- 타입 체크되지 않음:
-- _ : hd ≡ true
-- _ = refl
-- 대신 hd는 transport에 적용된 head를 포함하는 어떤 큰 표현식

정의가 transport에 걸려 있으면, 종종 가장 좋은 해결책은 그것이 되어야 하는 축약 가능한 표현식처럼 취급하지 않고 transport를 직접 관리하는 것이에요. 예를 들어 transport (sym p) (transport p x) ≡ x 증명을 사용해 hd를 정의적으로 걸려 있어도 경로까지는 계산할 수 있어요.

-- 위에서 계속..

  _ : hd ≡ true
  _ = cong head (transport⁻Transport (λ i → Vec Bool (p (~ i))) (true ∷ []))

다른 경우에는 패턴 매칭에서 비지원 경우를 피하도록 증명을 바꿔 표현하는 것이 가능해지고, 그래서 계산할 수 있어요. 예를 들어 sucInj로 돌아가, 우리는 그것을 (항상 계산하는) apEq와 suc가 부분적으로 정의된 역을 가진다는 사실로 정의할 수 있어요:

apEq : ∀ {a b} {A : Set a} {B : Set b} (f : A → B) {x y : A}
     → Eq x y → Eq (f x) (f y)
apEq f reflEq = reflEq

sucInjEq′ : ∀ {n k} → Eq (suc n) (suc k) → Eq n k
sucInjEq′ = apEq λ{ (suc n) → n ; zero → zero }

Cubical Agda와 호환되지 않는 원리(K, 타입 생성자의 단사성)에 의존하는 정의는 transport에 대해 결코 계산하지 않을 거예요. Cubical과 K를 둘 다 활성화하는 것은 --safe와 호환되지 않는다는 점에 유의하세요.

부정 절은 특별한 처리가 필요 없으므로(부정성의 transport는 여전히 부정성이므로), 귀납 타입의 생성자를 자동으로 분리하는 Agda의 능력에 의존하는 정의는 UnsupportedIndexedMatch 경고를 생성하지 않을 거예요.

zeroNotSucEq : ∀ {n} {a} {A : Set a} → Eq zero (suc n) → A
zeroNotSucEq ()

정교화가 Setω 타입에서 패턴 매칭으로부터 파생된 동등성을 사용하는 것을 포함하는 정의는 아직 확장될 수 없어요. 다음 예제는 Cubical 라이브러리의 예를 최소화하므로 매우 인위적이에요. 요점은 test를 transport를 포괄하도록 확장하려면 p : ℓ′ ≡ ℓ이 주어졌을 때 PathP (λ i → Argh ℓ (p i)) _ _를 만들어야 하는데, Setω가 아직 fibrant로 간주되지 않기 때문이에요.

data Argh (ℓ : Level) : Level → Setω where
  argh : ∀ {ℓ′} → Argh ℓ ℓ′ → Argh ℓ ℓ′

test : ∀ {ℓ ℓ′} → Argh ℓ ℓ′ → Bool
test {ℓ} (argh _) = true

모달리티와 인덱스된 매칭 (Modalities & indexed matching)

Cubical Agda에서 인덱스된 매칭을 사용할 때 절의 인자(와 그 오른쪽 변)는 인덱싱을 고려하기 위해 transport되어야 해서, 그 인자들의 타입이 잘 형성된 항이어야 함을 의미해요. 예를 들어 다음 코드는 Cubical Agda에서, 그리고 --without-K가 활성화될 때 금지돼요:

subst : (@0 P : A → Set p) → x ≡ y → P x → P y
subst _ refl p = p

술어 P가 소거되었기 때문이에요. 하지만 내부적으로 우리는 관련 위치에서 P를 포함하는 경로를 따라 인자 p를 transport해야 해요.

결과 타입에서 사용되거나 강제(점) 패턴 뒤에 나타나는 모든 인자는 모달리티-올바른 타입을 가져야 해요.

변형 (Variants)

변형 호환성 요약:

현재 \ 가져온 것	--cubical=no-glue	--cubical=erased	--cubical[=full]
--cubical=no-glue		--cubical=erased [1]	--cubical[=full] [1]

[1] --erasure가 활성화되고 소거된 위치에서 사용되는 경우에만. 아래 참고.

소거된 Glue를 가진 Cubical Agda (Cubical Agda with erased Glue)

--cubical=erased 옵션은 Glue(와 Agda.Builtin.Cubical.Glue에 정의된 다른 내장)가 소거된 설정에서만 사용되어야 하는 Cubical Agda의 변형을 활성화해요.

일반 Cubical Agda 코드는 --cubical=erased를 사용하는 코드를 임포트할 수 있어요. 일반 Cubical Agda 코드도 --cubical=erased를 사용하는 코드에서 임포트될 수 있지만, Cubical Agda로 정의된 이름은 --erasure 옵션이 사용될 때만 사용될 수 있어요. 그 경우 이름은 소거로 표시된 것처럼 취급되며, 패턴 매칭과 관련된 예외가 하나 있어요:

비-소거 가져온 생성자에 매칭하는 것 자체로는 Agda가 오른쪽 변을 소거된 것으로 취급하게 하지 않아요. 이 예외의 이유는 --cubical을 사용하는 모듈(에서 비-소거 생성자가 소거된 것으로 취급되지 않는)에서 코드를 임포트할 수 있어야 하기 때문이에요.

Cubical Agda 모듈에서 open import M args public으로 재-내보내진 이름은 Cubical Agda로 정의된 것으로 보인다는 점에 유의하세요.

Glue 없는 Cubical Agda (Cubical Agda without Glue)

--cubical=no-glue 옵션은 hcomp과 transp 같은 프리미티브가 여전히 사용 가능하지만 Glue 타입(과 Agda.Builtin.Cubical.Glue에 정의된 다른 내장)이 비활성화된 Cubical Agda의 변형(엄격한 부분집합)을 활성화해요. 따라서 이 변형에서는 항등 증명의 유일성(UIP) 또는 유니발런스 중 어느 하나를 postulate하는 것이 건전해야 하지만, 당연히 둘 다는 아냐. UIP와 호환되는 큐빅 타입 이론의 영감의 원천은 UIP가 정의적으로 성립하는 XTT예요.

현재 모듈이 --cubical=no-glue 옵션을 활성화하면:

Glue 타입의 사용을 (정도에 따라) 허용하므로 --cubical 또는 --cubical=erased 옵션이 있는 모듈에서는 임포트할 수 없어요.
현재 모듈에 의존하는 모듈은 Cubical(변형) 옵션 중 어느 하나를 활성화해야 해요: --cubical=no-glue, --cubical=erased, 또는 --cubical.

반면에 현재 모듈이 --cubical=erased 또는 --cubical 중 어느 것을 활성화하든, 항상 --cubical=no-glue가 있는 모듈을 임포트할 수 있어요.

참고 문헌 (References)

Cyril Cohen, Thierry Coquand, Simon Huber and Anders Mörtberg; "Cubical Type Theory: a constructive interpretation of the univalence axiom".
Thierry Coquand, Simon Huber, Anders Mörtberg; "On Higher Inductive Types in Cubical Type Theory".
Jonathan Sterling, Carlo Angiuli, Daniel Gratzer; "A Cubical Language for Bishop Sets".

부록: Cubical Agda 프리미티브 (Appendix: Cubical Agda primitives)

Cubical Agda 프리미티브와 내부는 Agda의 lib/prim/Agda/Builtin/Cubical 디렉터리에서 발견되는 일련의 파일들에 의해 내보내져요. agda/cubical 라이브러리는 이 문서 전체에서 사용된 이름들로 이 모든 프리미티브를 내보내요. 전문가는 agda/cubical이 실제로 내보내지 않는 꽤 많은 프리미티브가 사용 가능하므로 실제로 무엇이 내보내지는지 아는 것이 유용하다고 생각할 수 있어요. 그래서 이 섹션의 목표는 이 파일들의 내용을 나열하는 것이에요. 하지만 일반 사용자와 초보자에게는 agda/cubical 라이브러리로 충분하며 이 섹션은 안전하게 무시될 수 있어요.

경고: 정의가 Agda로 작성될 수 있는 많은 내장들이 그럼에도 cubical Agda 구현의 내부에서 사용되며, 다른 구현을 사용하면 쉽게 불건전성으로 이어질 수 있어요. 그것들이 사용자 코드에서 정의 가능할지라도, 이것은 지원되는 사용 사례가 아니에요.

프리미티브가 있는 핵심 파일은 Agda.Primitive.Cubical이에요. 그것은 다음 BUILTIN, 프리미티브와 postulate를 내보내요:

{-# BUILTIN CUBEINTERVALUNIV IUniv #-}  -- IUniv : SSet₁
{-# BUILTIN INTERVAL I  #-}  -- I : IUniv
{-# BUILTIN IZERO    i0   #-}
{-# BUILTIN IONE     i1   #-}

primitive
  primIMin : I → I → I   -- infixr 30 _∧_
  primIMax : I → I → I   -- infixr 30 _∨_
  primINeg : I → I       -- infix  20 ~_

{-# BUILTIN ISONE IsOne #-} -- IsOne : I → SSet

postulate
  itIsOne : IsOne i1     -- 1=1
  IsOne1  : ∀ i j → IsOne i → IsOne (primIMax i j)
  IsOne2  : ∀ i j → IsOne j → IsOne (primIMax i j)

{-# BUILTIN ITISONE      itIsOne  #-}
{-# BUILTIN ISONE1       IsOne1   #-}
{-# BUILTIN ISONE2       IsOne2   #-}
{-# BUILTIN PARTIAL      Partial  #-}
{-# BUILTIN PARTIALP     PartialP #-}

postulate
  isOneEmpty : ∀ {a} {A : Partial i0 (Set a)} → PartialP i0 A
{-# BUILTIN ISONEEMPTY isOneEmpty #-}

primitive
  primPOr : ∀ {a} (i j : I) {A : Partial (primIMax i j) (Set a)}
          → PartialP i (λ z → A (IsOne1 i j z)) → PartialP j (λ z → A (IsOne2 i j z))
          → PartialP (primIMax i j) A

  -- primHComp과 primTransp의 관점에서 계산
  primComp : ∀ {a} (A : (i : I) → Set (a i)) {φ : I} → (∀ i → Partial φ (A i)) → (a : A i0) → A i1

syntax primPOr p q u t = [ p ↦ u , q ↦ t ]

primitive
  primTransp : ∀ {a} (A : (i : I) → Set (a i)) (φ : I) → (a : A i0) → A i1
  primHComp : ∀ {a} {A : Set a} {φ : I} → (∀ i → Partial φ A) → A → A

구간 I는 자신만의 소트 IUniv에 속해요. 이 소트의 타입은 (Set과 달리) 합성과 transport를 지원하지 않지만, 이 소트의 타입에서 Set의 타입으로의 함수 타입은 (SSet과 달리) 지원해요.

경로 타입은 Agda.Builtin.Cubical.Path에 의해 내보내져요:

postulate
  PathP : ∀ {ℓ} (A : I → Set ℓ) → A i0 → A i1 → Set ℓ

{-# BUILTIN PATHP        PathP     #-}

infix 4 _≡_
_≡_ : ∀ {ℓ} {A : Set ℓ} → A → A → Set ℓ
_≡_ {A = A} = PathP (λ _ → A)

{-# BUILTIN PATH         _≡_     #-}

큐빅 부분타입은 Agda.Builtin.Cubical.Sub에 의해 내보내져요:

{-# BUILTIN SUB Sub #-}

postulate
  inc : ∀ {ℓ} {A : Set ℓ} {φ} (x : A) → Sub A φ (λ _ → x)

{-# BUILTIN SUBIN inS #-}

primitive
  primSubOut : ∀ {ℓ} {A : Set ℓ} {φ : I} {u : Partial φ A} → Sub _ φ u → A

동치는 Agda.Builtin.Cubical.Equiv에 의해 내보내져요:

record isEquiv {ℓ ℓ'} {A : Set ℓ} {B : Set ℓ'} (f : A → B) : Set (ℓ ⊔ ℓ') where
  field
    equiv-proof : (y : B) → isContr (fiber f y)
infix 4 _≃_

_≃_ : ∀ {ℓ ℓ'} (A : Set ℓ) (B : Set ℓ') → Set (ℓ ⊔ ℓ')
A ≃ B = Σ (A → B) λ f → isEquiv f

equivFun : ∀ {ℓ ℓ'} {A : Set ℓ} {B : Set ℓ'} → A ≃ B → A → B
equivFun e = fst e

equivProof : ∀ {la lt} (T : Set la) (A : Set lt) → (w : T ≃ A) → (a : A)
           → ∀ ψ (f : Partial ψ (fiber (w .fst) a)) → fiber (w .fst) a [ ψ ↦ f ]
equivProof A B w a ψ fb = contr' {A = fiber (w .fst) a} (w .snd .equiv-proof a) ψ fb
  where
    contr' : ∀ {ℓ} {A : Set ℓ} → isContr A → (φ : I) → (u : Partial φ A) → A
    contr' {A = A} (c , p) φ u = hcomp (λ{ i (φ = i1) → p (u 1=1) i
                                         ; i (φ = i0) → c }) c

{-# BUILTIN EQUIV      _≃_        #-}
{-# BUILTIN EQUIVFUN   equivFun   #-}
{-# BUILTIN EQUIVPROOF equivProof #-}

Glue 타입은 Agda.Builtin.Cubical.Glue에 의해 내보내져요:

open import Agda.Builtin.Cubical.Equiv public

primitive
  primGlue    : ∀ {ℓ ℓ'} (A : Set ℓ) {φ : I}
    → (T : Partial φ (Set ℓ')) → (e : PartialP φ (λ o → T o ≃ A))
    → Set ℓ'
  prim^glue   : ∀ {ℓ ℓ'} {A : Set ℓ} {φ : I}
    → {T : Partial φ (Set ℓ')} → {e : PartialP φ (λ o → T o ≃ A)}
    → PartialP φ T → A → primGlue A T e
  prim^unglue : ∀ {ℓ ℓ'} {A : Set ℓ} {φ : I}
    → {T : Partial φ (Set ℓ')} → {e : PartialP φ (λ o → T o ≃ A)}
    → primGlue A T e → A
  primFaceForall : (I → I) → I

agda/cubical에서는 Glue 타입이 더 사용하기 편하도록 커리되지 않는다(uncurried)는 점에 유의하세요:

Glue : ∀ {ℓ ℓ'} (A : Set ℓ) {φ : I}
     → (Te : Partial φ (Σ[ T ∈ Set ℓ' ] T ≃ A))
     → Set ℓ'
Glue A Te = primGlue A (λ x → Te x .fst) (λ x → Te x .snd)

더 알아보기 (Learn more)

Agda 문서: 큐빅 원문