<div dir="ltr">{-<br>The fixed-point definition in section 2.3 of <a href="https://www.researchgate.net/publication/228944016_Generic_Programming_with_Indexed_Functors">Generic Programming with Indexed Functors</a> no longer type-checks in the latest version of Agda, which complains that μ is not strictly positive:<br><br>  data μ {I O : Set} (F : (I ⊎ O) ▶ O) (r : Indexed I) (o : O) : Set where<br>    ⟨_⟩ : ⟦ F ⟧ (r ∣ μ F r) o → μ F r o<br><br>I haven&#39;t had any luck finding a workaround. The code below is ripped from the article and reproduces the problem I&#39;m having. Thanks in advance for any help solving this.<br>-}<br><br>module IndexedFunctor where<br>  open import Function using (_∘_)<br>  open import Relation.Binary.Core using (_≡_)<br><br>  open import Data.Empty using (⊥)<br>  open import Data.Unit using (⊤ ; tt)<br>  <br>  open import Data.Product using (_×_ ; ∃)<br>  open import Data.Sum using (_⊎_ ; inj₁ ; inj₂)<br>  <br>  Indexed : Set → Set₁<br>  Indexed I = I → Set<br><br>  _▷_ : Set → Set → Set₁<br>  I ▷ O = Indexed I → Indexed O<br><br>  record _≃_ (A B : Set) : Set where<br>    field<br>      from : A → B<br>      to   : B → A<br>      iso₁ : ∀ {x} → to (from x) ≡ x<br>      iso₂ : ∀ {x} → from (to x) ≡ x<br><br>  _∣_ : ∀ {A B} → Indexed A → Indexed B → Indexed (A ⊎ B)<br>  _∣_ ia _ (inj₁ x) = ia x<br>  _∣_ _ ib (inj₂ x) = ib x<br><br>  mutual<br>    data _▶_ : Set → Set → Set₁ where<br>      Z      : ∀ {I O} → I ▶ O<br>      U      : ∀ {I O} → I ▶ O<br>      I      : ∀ {I O} → I → I ▶ O<br>      !      : ∀ {I O} → O → I ▶ O<br>      _⊕_    : ∀ {I O}   → I ▶ O → I ▶ O → I ▶ O<br>      _⊗_    : ∀ {I O}   → I ▶ O → I ▶ O → I ▶ O<br>      _⊚_    : ∀ {I M O} → M ▶ O → I ▶ M → I ▶ O<br>      _↗_↘_  : ∀ {I I&#39; O O&#39;} → I&#39; ▶ O&#39; → (I&#39; → I) → (O → O&#39;) → I ▶ O<br>      Fix    : ∀ {I O} → (I ⊎ O) ▶ O → I ▶ O<br>      ∑      : ∀ {I O} → {C : ⊥ ▶ ⊤} → (⟦ C ⟧ (λ _ → ⊤) tt → I ▶ O) → I ▶ O<br>      Iso    : ∀ {I O} → (C : I ▶ O) → (D : I ▷ O) → ((r : Indexed I) → (o : O) → D r o ≃ ⟦ C ⟧ r o) → I ▶ O<br><br>    data μ {I O : Set} (F : (I ⊎ O) ▶ O) (r : Indexed I) (o : O) : Set where<br>      ⟨_⟩ : ⟦ F ⟧ (r ∣ μ F r) o → μ F r o<br>   <br>    ⟦_⟧ : ∀ {I O} → I ▶ O → I ▷ O<br>    ⟦ Z         ⟧ r o = ⊥<br>    ⟦ U         ⟧ r o = ⊤<br>    ⟦ I i       ⟧ r o = r i<br>    ⟦ F ↗ f ↘ g ⟧ r o = ⟦ F ⟧ (r ∘ f) (g o)<br>    ⟦ F ⊕ G     ⟧ r o = ⟦ F ⟧ r o ⊎ ⟦ G ⟧ r o<br>    ⟦ F ⊗ G     ⟧ r o = ⟦ F ⟧ r o × ⟦ G ⟧ r o<br>    ⟦ F ⊚ G     ⟧ r o = ⟦ F ⟧ (⟦ G ⟧ r) o<br>    ⟦ Fix F     ⟧ r o = μ F r o<br>    ⟦ ! o&#39;      ⟧ r o = o ≡ o&#39;<br>    ⟦ ∑ f       ⟧ r o = ∃ (λ i → ⟦ f i ⟧ r o)<br>    ⟦ Iso C D e ⟧ r o = D r o<br><br clear="all"><div><div class="gmail_signature"><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr">--<br>Martin Stone Davis<br><div><br>Postal/Residential:<br></div><div style="margin-left:40px"><span>1223 Ferry St</span><span><span><br></span></span></div><div style="margin-left:40px"><span><span>Apt 5<br></span></span></div><div style="margin-left:40px"><span>Eugene, OR 97401</span><br></div>Talk / <span></span>Text / Voicemail: <a href="tel:3106993578" value="+13106993578" target="_blank">(310) 699-3578</a><br>Electronic Mail: <a href="mailto:martin.stone.davis@gmail.com" target="_blank">martin.stone.davis@gmail.com</a><div><div><div><span></span></div></div></div></div></div><div dir="ltr"><span style="font-size:small">Website: </span><a href="http://martinstonedavis.com/" style="color:rgb(17,85,204);font-size:small" target="_blank">martinstonedavis.com</a></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div>
</div>