단일 값을 가진 유형 정의

Question

여기에서 : 슬라이드 23의 http://www.cse.chalmers.se/~coquand/equality.pdf은 매우 흥미로운 유형 인 iscontr A을 정의합니다. 나는 그것이 다음과 같이 해석한다고 생각한다 :

record iscontr {A : Set} : Set where 
    constructor _exists_unique 
    field 
    a : A 
    singleton : (x : A) -> a == x 

나는 그들이 만드는 미묘한 점을 보지 못했다. 그들은 처음에 이것이 단지 복수의, 그러나 (경로) 연결 된 가치가있는 단지 증거라고 보일 수 있다고 주장합니다 - 이것은 정확히 제가 여기서 보는 것입니다; 그러나 실제로, 그들은 주장한다, 유형 A에있는 단일 주민이있는의 증거이다.

심지어 J이 도입되기 전에 (유도 공리의 대체 정의를 제공하기 위해 실제로 사용되는 경우)이 사실은 유도 이외의 것으로부터 비롯된 것이어야합니다.

좋아, 처음에 나는이 유형의 서식에 그 유형 A의 어떤 값을 매핑 할 수있는 기능을 생산하는 것을 의미 생각 - 기억 ((예 공리에 의해 소개) 정규없는 것을 포함을 우리는 할 수 없습니다 우리는 유도 공리 (induction axiom)가 아직 없기 때문에 여기에서 일반적인 패턴 매칭을해라.) 이것은 공리를 사용하더라도 어떤 식 으로든 새로운 값을 A에 추가 할 수 없다는 것을 의미합니다. 이 사실은 우리가 꽤 많은 타입의 사람들 (다음 슬라이드에서 타입 (x, α)을 위해하는 것입니다)을 통해 iscontr 타입의 주민을 소개하겠다는 분명한 징후입니다. 그러나 이것이 각각 을 생성하는 함수에 열거 된 A 유형의 다중 값의 존재를 어떻게 배제하는지 보지 못합니다.

(또한, 나는 등 toposes, groupoids에서 예제를 이해하지 못할, 그래서 23 슬라이드 이전에 도입 공리를 기반으로 일반 추론을 통해 설명을보고 좋은 것) 아마

Answer 1

설득하는 가장 좋은 방법 당신은 is-contr A이 실제로는 A에 단일 주민이 있다는 것을 의미합니다. 이전에 주석에서 언급했듯이, 모든 수축 가능 유형과 단위 유형간에 동등한 것을 보여주는 것입니다. 우리는 이미 수축성이

, 그러나 저 대신이 포켓 버전을 사용하자 :이, 나는 몇 가지 정의가 필요합니다

is-contr : ∀ {a} (A : Set a) → Set _ 
is-contr A = Σ A λ a → ∀ x → a ≡ x 

다음을 : 동등성. 그것은 왼쪽과 모두있는 경우

_≃_ : ∀ {a b} (A : Set a) (B : Set b) → Set _ 
A ≃ B = Σ (A → B) is-equiv 

그래서, 함수 f는 등가입니다 :

-- Homotopies. 
infix 1 _~_ 

_~_ : ∀ {a b} {A : Set a} {B : A → Set b} 
    (f g : ∀ a → B a) → Set _ 
f ~ g = ∀ x → f x ≡ g x 

-- Equivalence. 
is-equiv : ∀ {a b} {A : Set a} {B : Set b} 
    (f : A → B) → Set _ 
is-equiv {A = A} {B = B} f 
    = (Σ (B → A) λ g → f ∘ g ~ id) 
    × (Σ (B → A) λ h → h ∘ f ~ id) 

그리고 마지막으로 : 나는 HOTT 책 전반에 걸쳐 사용되는 is-equiv 버전을 사용하는거야 오른쪽 반대.

이이 기능 f 한 쌍의 g 등이 f ∘ g ~ id 및 g ∘ f ~ id, 실제로 당신에게 동등한 (동형)의 일반적인 정의를 생각 나게한다, 그것은 위의 정의 (증거에 대한이 답변에 의견을 참조 논리적으로 동일하다).

어쨌든, 우리는 지금 마지막 문 공식화 할 수 있습니다

contr-≃⊤ : ∀ {a} {A : Set a} → is-contr A → A ≃ ⊤ 

증거 오히려 간단하다

contr-≃⊤ : ∀ {a} {A : Set a} → is-contr A → A ≃ ⊤ 
contr-≃⊤ (a , p) 
    = (λ _ → tt) 
    , ((λ _ → a) , (λ _ → refl)) 
    , ((λ _ → a) , p) 

그래서, 우리의 왼쪽과 오른쪽 역은 선택한 요소에 불과 일정 기능입니다 (에서).

연계성은 HOTT 책에 정의 된대로, 사실,이 동등성을 입증 할 수 없습니다

is-conn : ∀ {a} (A : Set a) → Set _ 
is-conn A = Σ A λ a → ∀ x → ∥ a ≡ x ∥ 

(I는 유니 코드 문자가 당신을 위해 표시를 바란다).

contr-≃⊤ (a , p) 
    = (λ _ → tt) 
    , ((λ _ → a) , (λ _ → refl)) 
    , ((λ _ → a) , (λ x → p x)) 

우리는 이것을 증명 할 수 a에서 x (즉 p x : a ≡ x)에 실제 경로를 알 필요가 : 당신이 도착 예정 contr-≃⊤ 증거에 p을 확장 할 때이 가장 잘 알 수있다. 그러나 ∥ a ≡ x ∥은 훨씬 약하다 - 그것은 단지 그러한 경로가 존재하지만 우리에게 경로가 어떻게 보이는지 알려주지 않는다. 유형 이론 (대신 공리의) 선택의 정리을 왜

---

이는 이유입니다. 실존 적 정량화의 건설적인 본성은 증거를 사소한 것으로 만든다. 그러나 실제 거주자에 관한 정보를 지우고 그러한 사실 만 남겨두면 그 중 하나가 선택의 평범한 원칙을 얻게됩니다. 원하는 경우, HoTT 책의 3.7 장과 3.8 장을 확인하십시오.