<div dir="ltr"><div>Dear all,</div><div><br></div><div>I'm using the agda standard lib from git:<br>commit 853e309e55bdc80407564e44396751a84e8c55f0 <br><br></div><div>~/agda-stdlib/src/Data/Nat/DivMod.agda:205,1-47<br>Agda.Primitive.Cubical.primTransp<br>(λ i →<br>   m /<br>   Agda.Primitive.Cubical.primComp (λ i₁ → ℕ)<br>   (λ i₁ .o →<br>      Agda.Primitive.Cubical.primPOr<br>      (Agda.Primitive.Cubical.primIMax<br>       (Agda.Primitive.Cubical.primINeg i) φ)<br>      i (λ .o₁ → suc m₁) (λ .o₁ → x i₁) _)<br>   (suc m₁)<br>   ≤ n / x₁ i)<br>φ (/-mono-≤ x₂ (s≤s x₃)) is not usable at the required modality<br>when checking the definition of /-mono-≤<br></div><div><br>$ agda --version<br>Agda version 2.6.3-78ea6d2<br><br></div><div>Is this a known error, or is there a problem on my agda configuration?</div><div><br></div><div>Thanks & regards<br><br></div><div>Steve <br>(from Vienna)<br></div><div><br></div></div>