（n + 1）型の型は、（n）型に依存します）

Question

私はintentivly型を定義したいと思います。 私が（nt + 1）を定義している間、（urt n）について何か知りたいです。 idenitifier sigTは、従属ペアのタイプを作成します。 pr1、pr2はそのようなペアからの投影です。

Context (qsigT: forall (A : Type) (P : forall a : A, Type), Type). 
Context (qpr1: forall (A : Type) (P : forall a : A, Type), (@qsigT A P) -> A). 
Inductive Unit : Type := 
    | tt : Unit. 
Inductive Bool : Type := 
    | true : Bool 
    | false : Bool. 
Fixpoint urt (n:nat): Type. 

Proof. 
    refine (@qsigT Bool _). 

    destruct n. 

    exact (fun _ => Unit). 
    exact (fun q => 
      (@qsigT (urt n) (fun q => (*error below occurs because of using (urt n)*) 
      Unit+Unit+Unit (*I also cannot use here something like (qpr1 q), because of the same reasons*) 
     )) 
). 
    Show Proof. 

Defined. 
Check fun (q : urt 4) => qpr1 q. (*Error!*) 

Context (y:nat). 
Check fun (q : urt y) => qpr1 q. (*Error here, need to be solved*) 

エラーがどのように定義を変更する必要があり The term "q" has type "urt (S (S (S (S O))))" while it is expected to have type "Type". のですか？

Answer 1

urtの定義にはトップレベルの固定点がありますので、固定点はsigT _ _形式に縮小するためにはyを破棄する必要があります。 （ヒント：お客様のCheckステートメントで(S y)を使用してみてください）。

あなたが何をしたいのかは分かりませんが、sigTコンストラクタの後に固定点を遅らせることが考えられます。

Definition urt (n : nat) : Type. 
Proof. 
    refine (@qsigT Bool _). 
    revert n. 
    fix urt 1. 
    intros [|n]. 
    exact (fun _ => Unit). 
    exact (fun q => 
      (@qsigT (urt n q) (fun q => (*error below occurs because of using (urt n)*) 
      (Unit+Unit+Unit)%type (*I also cannot use here something like (qpr1 q), because of the same reasons*) 
     )) 
). 
    Show Proof. 

Defined. 
Check fun (q : urt 4) => qpr1 _ _ q. 
Context (y:nat). 
Check fun (q : urt y) => qpr1 _ _ q.