agda의 우주 계량화

Question

나는 문제를 발견하고 우주 계량화를 추가 할 수있었습니다.

하지만 누군가 진짜로 무슨 일이 벌어지면 재미있을 것입니다.

module Level0Equality (A : Set) where 
    data _Tauto'_ : A → A → Set where 
    refl2 : (a : A) → a Tauto' a 

    -- universe quantified 
    data _Tauto_ {l} {A : Set l} : A → A → Set l where 
    refl2 : (a : A) → a Tauto a 

    -- PEq x = the type of proof that y ≡ x 
    data PEq {A : Set} (x : A) : Set where 
    it : (y : A) -> (y Tauto x) -> PEq x 

    -- does not work because of lack of universe quantification in Tauto' 
    -- A !=< A of type Set 
    -- (because one has deBruijn index 2 and the other 3) 
    -- when checking that the expression y has type A 
    data PEq' {A : Set} (x : A) : Set where 
    it : (y : A) -> (y Tauto' x) -> PEq' x 

Answer 1

문제는 PEq' 당신의 정의는 Set에서 어떤 A 작동 있음을 알 수 있다는 것입니다. 그러나 _Tauto'_은 사용자가 Level0Equality에 모듈 매개 변수로 제공하는 특정 A에 대해서만 작동합니다.

내가 예와 함께 설명하자

open Level0Equality Bool 

_Tauto'_ : Bool → Bool → Set 
PEq' : {A : Set} → A → Set 

다음 우리가, 우리가 A = String 선택 말 : 이것은 분명히 PEq'.it 생성자에 문제를 일으킬 수

PEq' {A = String} : String → Set 

. x과 y의 유형이 모두 String이지만, _Tauto'_은 Bool!에만 적용됩니다.

---

수정 사항은 간단합니다. 모듈 망원경에서 A을 사용하십시오.

data PEq' (x : A) : Set where 
    it : (y : A) -> (y Tauto' x) -> PEq' x