<div dir="ltr"><div>Hi David,</div><div><br></div><div>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.<br></div><div><br></div><div>```agda</div><div>open import Agda.Primitive<br>open import Agda.Builtin.Nat<br>open import Agda.Builtin.Equality<br>open import Agda.Builtin.Unit<br>open import Agda.Builtin.Sigma<br><br>variable<br>  l : Level<br>  A B C : Set l<br><br>data ⊥ : Set where<br></div><div><br>{-# NO_UNIVERSE_CHECK #-} -- disables universe level check locally<br>data TypedPath {l}  : Set l -> Set l -> Set l where<br>   atom : ∀ {A B : Set l} -> A -> B -> TypedPath A B<br>   append : ∀ {A B C : Set l} -> (A -> C) -> TypedPath C B ->  TypedPath A B<br><br>data D : TypedPath ⊥ ⊤ → Set where<br>  c : (A : Set) → D (append {C = A} (λ ()) (append (λ _ → tt) (atom tt tt)))<br><br>Set′ : Set<br>Set′ = Σ (TypedPath ⊥ ⊤) D<br><br>box : Set → Set′<br>box A = _ , c A<br><br>unbox : Set′ → Set<br>unbox (_ , c A) = A<br><br>box-unbox : ∀ X → box (unbox X) ≡ X<br>box-unbox (_ , c A) = refl<br><br>unbox-box : ∀ A → unbox (box A) ≡ A<br>unbox-box A = refl</div><div>```</div><div><br></div><div>-- Jesper<br></div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Tue, Jun 4, 2019 at 3:51 PM <<a href="mailto:david.janin@labri.fr">david.janin@labri.fr</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">Dear all, <br>
<br>
Could well be a silly question, but I don’t understand why the following definition does not type in Agda:<br>
<br>
data TypedPath {l}  : Set l -> Set l -> Set l where<br>
   atom : ∀ {A B : Set l} -> A -> B -> TypedPath A B<br>
   append : ∀ {A B C : Set l} -> (A -> C) -> TypedPath C B ->  TypedPath A B<br>
<br>
Instead, it seems that Agda expects<br>
<br>
data TypedPath {l}  : Set l -> Set l -> Set (suc l) where<br>
   ….<br>
<br>
with an increase in type universe level. <br>
<br>
<br>
As far as I eventually manage to make CoQ prints its (more hidden) universe levels, the inductive type<br>
<br>
Inductive hybridPath : Type -> Type -> Type :=<br>
  const: forall A B : Type,  A  -> B -> hybridPath A A<br>
| comp : forall A B C : Type, hybridPath A C <br>
       -> hybridPath C B -> hybridPath A B.<br>
<br>
stays in CoQ within the same level of types….<br>
<br>
Any hint welcome,<br>
<br>
David<br>
<br>
<br>
_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</blockquote></div>