[Agda] Type level computation in inductive types

[Jesper Cockx]

Hi David,

The reason why your TypedPath type is rejected is because C (the third
implicit argument of append) lives in universe Set l, but unlike A and B it
is not forced by the indices of the type of append. If it were accepted,
then you would be able to store a value of type Set l in a (relatively)
small datatype which lives in Set l itself. Indeed, if this type were
allowed we could define a type Set′ : Set which is isomorphic to Set itself.

```agda
open import Agda.Primitive
open import Agda.Builtin.Nat
open import Agda.Builtin.Equality
open import Agda.Builtin.Unit
open import Agda.Builtin.Sigma

variable
  l : Level
  A B C : Set l

data ⊥ : Set where

{-# NO_UNIVERSE_CHECK #-} -- disables universe level check locally
data TypedPath {l}  : Set l -> Set l -> Set l where
   atom : ∀ {A B : Set l} -> A -> B -> TypedPath A B
   append : ∀ {A B C : Set l} -> (A -> C) -> TypedPath C B ->  TypedPath A B

data D : TypedPath ⊥ ⊤ → Set where
  c : (A : Set) → D (append {C = A} (λ ()) (append (λ _ → tt) (atom tt tt)))

Set′ : Set
Set′ = Σ (TypedPath ⊥ ⊤) D

box : Set → Set′
box A = _ , c A

unbox : Set′ → Set
unbox (_ , c A) = A

box-unbox : ∀ X → box (unbox X) ≡ X
box-unbox (_ , c A) = refl

unbox-box : ∀ A → unbox (box A) ≡ A
unbox-box A = refl
```

-- Jesper

On Tue, Jun 4, 2019 at 3:51 PM <david.janin at labri.fr> wrote:

> Dear all,
>
> Could well be a silly question, but I don’t understand why the following
> definition does not type in Agda:
>
> data TypedPath {l}  : Set l -> Set l -> Set l where
>    atom : ∀ {A B : Set l} -> A -> B -> TypedPath A B
>    append : ∀ {A B C : Set l} -> (A -> C) -> TypedPath C B ->  TypedPath A
> B
>
> Instead, it seems that Agda expects
>
> data TypedPath {l}  : Set l -> Set l -> Set (suc l) where
>    ….
>
> with an increase in type universe level.
>
>
> As far as I eventually manage to make CoQ prints its (more hidden)
> universe levels, the inductive type
>
> Inductive hybridPath : Type -> Type -> Type :=
>   const: forall A B : Type,  A  -> B -> hybridPath A A
> | comp : forall A B C : Type, hybridPath A C
>        -> hybridPath C B -> hybridPath A B.
>
> stays in CoQ within the same level of types….
>
> Any hint welcome,
>
> David
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20190604/c19d85a9/attachment.html>