Salut,

Je vous montre le problème lié aux types inductifs que j’ai mentionné hier.

On définit d’abord le type `Sigma`

Sigma = typecons (Sigma (l1 ::: TypeLevel) (l2 ::: TypeLevel) (A : Type_ l1) (B : A -> Type_ l2)) (sigma (fst : A) (snd : B fst)); sigma = datacons Sigma sigma;

Mais quand il s’agit de construire une expression de ce type, on se retrouve dans l’obligation de fournir la valeur de `B` explicitement lors de la construction même si l’information se trouve déjà dans l’annotation de type.

up : Sigma Unit (lambda _ -> Unit);; up = sigma (B := lambda _ -> Unit) unit unit; %% ça ne marche plus si on enlève l’argument B

Si on enlève le B, on obtient l’erreur "Context expected: (?B↑0 unit) but expression has type: Unit”. J’ai investigué un tout petit peu, mais malheureusement j’ai pas pu trouver la source de ce problème.

J’ai rencontré un autre problème avec les indices de Debruijn quand j’écrivais cette preuve

HoTT_isContr A = Sigma A (lambda (x : A) -> ((y : A) -> Eq x y));

isContrΠ : (A : Type_ ?) ≡> (B : A -> Type_ ?) ≡> (h : (x : A) -> HoTT_isContr (B x)) -> HoTT_isContr ((x : A) -> B x); isContrΠ h = sigma (A := (x : A) -> B x) (B := (lambda (x : ((x : A) -> B x)) -> ((y : ((x : A) -> B x)) -> Eq x y))) (lambda x -> case (h x) | sigma bx p => bx) (lambda f -> Eq_eq (f := lambda i ≡> lambda x -> case (h x) | sigma bx p => Eq_uneq (p := p (f x)) (i := i)));

qui donnait l’erreur

[X] Fatal :(DEBRUIJN) DeBruijn index 2 refers to wrong name. Expected: " %gensym% no 42 “ got " %gensym% no 39 “

On rencontre ce problème quand on est dans la branche du 2e `case` dans le code. Mon hypothèse est que le `bx` n’est pas égal à l’autre `bx` dans le 1er `case`, et puisque ce que renvoit le 2e `case` dépend de ce qui est renvoyé dans l’autre, ça devient un problème. La bonne nouvelle c’est que j’ai réussi à contourner le problème en remplaçant les deux `case ` par des appels à des fonctions auxiliaires.

pr1 : Sigma ?A ?B -> ?A; pr1 s = case s | sigma a _ => a;

pr2 : (s : Sigma ?A ?B) -> ?B (pr1 s); pr2 = lambda _ _ A B ≡> lambda s -> case s | sigma a b => let branch=s : Eq (sigma (A := A) (B := B) a b) s; branch=s = ##DeBruijn 0; res : B (pr1 s); res = Eq_cast (p := branch=s) (f := lambda x -> B (pr1 x)) b; in res;

isContrΠ : (A : Type_ ?) ≡> (B : A -> Type_ ?) ≡> (h : (x : A) -> HoTT_isContr (B x)) -> HoTT_isContr ((x : A) -> B x); isContrΠ = lambda _ _ A B ≡> lambda h -> sigma (A := (x : A) -> B x) (B := (lambda (x : ((x : A) -> B x)) -> ((y : ((x : A) -> B x)) -> Eq x y))) (lambda x -> pr1 (h x)) (lambda g -> Eq_eq (f := lambda i ≡> lambda x -> Eq_uneq (p := (pr2 (h x)) (g x)) (i := i)));

A première vue, c’est peut-être lié à un problème similaire dans `hurkens.typer` (regardez la ligne 87). Pour faciliter la reproduction de ces bugs, j’ai attaché en pièce jointe un fichier qui contient tout le code que j’ai montré ci-dessus.

James