Agda

Question

में टाइप पदानुक्रम टाइप करें मैं यह पता लगाने की कोशिश कर रहा हूं कि एजडा में पदानुक्रम कैसे काम करते हैं।

मान लिया जाये कि मैं एक सेट प्रकार एक्स परिभाषित:

X : Set 

और फिर एक आगमनात्मक प्रकार

data Y : X -> Set where 

X -> Set के प्रकार क्या है के निर्माण के लिए आगे बढ़ें? क्या यह सेट या टाइप है?

धन्यवाद!

Answer 1

ठीक है, आगडा से खुद क्यों नहीं पूछें? मैं Emacs के लिए उत्कृष्ट Agda मोड का उपयोग करने जा रहा हूँ। हम शुरू से:

module Hierarchy where 

postulate 
    X : Set 

data Y : X → Set where 
    -- empty 

हम C-c C-l का उपयोग कर फ़ाइल को लोड करने के लिए है; यह फ़ाइल टाइपशेक करता है, ? एस छेद में बदल जाता है, सिंटैक्स हाइलाइटिंग करता है और इसी तरह।

> C-c C-d 
Expression: 
> Y 
X → Set 

ठीक है, कि समझ में आता है:

अब, वहाँ एक कमांड C-c C-d के माध्यम से "अनुमान कर (अनुमान) टाइप" उपलब्ध है, तो चलो कि का उपयोग करते हैं है। हमने Y : X → Set परिभाषित किया है, इसलिए इसे कोई आश्चर्य नहीं होना चाहिए। आइए फिर से पूछें:

> C-c C-d 
Expression: 
> X → Set 
Set₁ 

तो, आपके पास यह है: Y : X → Set : Set₁।

---

जबकि पहला भाग प्रश्न का उत्तर देता है और आपको दिखाता है कि इस सामान को स्वयं कैसे जांचें, ऐसा करने से हर समय कमजोर होगा। यहाँ यह कैसे काम करता है:

विरोधाभास से बचने के लिए, हम

Set i : Set (i + 1) 

जो आप Set एस के (अनंत) पदानुक्रम देता है की आवश्यकता है। यदि आपके पास Set : Set था (जो एग्डा --type-in-type ध्वज के माध्यम से अनुमति देता है), तो आप this one जैसे विरोधाभास प्राप्त कर सकते हैं।

A : Set i 
B : A → Set j 

(a : A) → B a : Set (max i j) 

आपके उदाहरण में आवेदन::

X : Set 
Set : Set₁ 

X → Set : Set (max 0 1) 
X → Set : Set₁