<div dir="ltr"><div>I stopped work on re-implementing it when I became disheartened, finding out that the original work was done by disabling the positivity and termination checkers. I couldn't see a way to do it with those checkers enabled. <br></div></div><div class="gmail_extra"><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>
<br><div class="gmail_quote">On Sun, Jan 24, 2016 at 10:10 PM, Kenichi Asai <span dir="ltr"><<a href="mailto:asai@is.ocha.ac.jp" target="_blank">asai@is.ocha.ac.jp</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Dear Martin,<br>
<br>
It appears you are re-implementing the Indexed Functors using the Agda<br>
standard library. Do you make the code available somewhere?<br>
<span class="HOEnZb"><font color="#888888"><br>
--<br>
Kenichi Asai<br>
</font></span><div class="HOEnZb"><div class="h5"><br>
<br>
On Wed, Jan 06, 2016 at 08:03:35PM -0800,<br>
Martin Stone Davis wrote:<br>
<br>
> {-<br>
> The fixed-point definition in section 2.3 of Generic Programming with Indexed<br>
> Functors no longer type-checks in the latest version of Agda, which complains<br>
> 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't had any luck finding a workaround. The code below is ripped from the<br>
> article and reproduces the problem I'm having. Thanks in advance for any help<br>
> 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' O O'} → I' ▶ O' → (I' → I) → (O → O') → 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)<br>
> → 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' ⟧ r o = o ≡ o'<br>
> ⟦ ∑ f ⟧ r o = ∃ (λ i → ⟦ f i ⟧ r o)<br>
> ⟦ Iso C D e ⟧ r o = D r o<br>
><br>
> --<br>
> Martin Stone Davis<br>
><br>
> Postal/Residential:<br>
> 1223 Ferry St<br>
> Apt 5<br>
> Eugene, OR 97401<br>
> Talk / Text / Voicemail: (310) 699-3578<br>
> Electronic Mail: <a href="mailto:martin.stone.davis@gmail.com">martin.stone.davis@gmail.com</a><br>
> Website: <a href="http://martinstonedavis.com" rel="noreferrer" target="_blank">martinstonedavis.com</a><br>
<br>
</div></div><div class="HOEnZb"><div class="h5">> _______________________________________________<br>
> Agda mailing list<br>
> <a href="mailto:Agda@lists.chalmers.se">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>
</div></div></blockquote></div><br></div>