Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
Inductive-recursive and infinitary version of https://gist.github.com/larrytheliquid/e2bec348c9fb7d894ff25e61efa0349c
open import Data.Unit
open import Data.Product
module _ where
----------------------------------------------------------------------
data Desc (I : Set) (O : I Set) : Set₁ where
: (i : I) (o : O i) Desc I O
: (A : Set) (i : A I) (D : (o : (a : A) O (i a)) Desc I O) Desc I O
: (A : Set) (D : A Desc I O) Desc I O
mutual
data μ {I O} (R : I Desc I O) (i : I) : I Set where
init : (xs : ⟦ R i ⟧ R) μ R i (proj₁ (io (R i) R xs))
ode : {I O} (R : I Desc I O) (i j : I) μ R i j O j
ode R i ._ (init xs) = proj₂ (io (R i) R xs)
⟦_⟧ : {I O} (D : Desc I O) (R : I Desc I O) Set
⟦ `ι i o ⟧ R =
⟦ `δ A i D ⟧ R = Σ ((a : A) μ R (i a) (i a)) λ f ⟦ D (λ a ode R (i a) (i a) (f a)) ⟧ R
⟦ `σ A D ⟧ R = Σ A λ a ⟦ D a ⟧ R
io : {I O} (D : Desc I O) (R : I Desc I O) (xs : ⟦ D ⟧ R) Σ I O
io (`ι i o) R tt = i , o
io (`δ A i D) R (f , xs) = io (D (λ a ode R (i a) (i a) (f a))) R xs
io (`σ A D) R (a , xs) = io (D a) R xs
----------------------------------------------------------------------
Hyps : {I O} (R : I Desc I O) (P : (i j : I) μ R i j Set) (D : Desc I O) (xs : ⟦ D ⟧ R) Set
Hyps R P (`ι i o) tt =
Hyps R P (`σ A D) (a , xs) = Hyps R P (D a) xs
Hyps R P (`δ A i D) (f , xs) = ((a : A) P (i a) (i a) (f a))
× Hyps R P (D (λ a ode R (i a) (i a) (f a))) xs
----------------------------------------------------------------------
ind :
{I O}
(R : I Desc I O)
(P : (i j : I) μ R i j Set)
(pcon : (i : I) (xs : ⟦ R i ⟧ R) Hyps R P (R i) xs P i (proj₁ (io (R i) R xs)) (init xs))
(i j : I)
(x : μ R i j)
P i j x
hyps :
{I O}
(R : I Desc I O)
(P : (i j : I) μ R i j Set)
(pcon : (i : I) (xs : ⟦ R i ⟧ R) Hyps R P (R i) xs P i (proj₁ (io (R i) R xs)) (init xs))
(D : Desc I O)
(xs : ⟦ D ⟧ R)
Hyps R P D xs
ind R P pcon i j (init xs) = pcon i xs (hyps R P pcon (R i) xs)
hyps R P pcon (`ι i o) tt = tt
hyps R P pcon (`σ A D) (a , xs) = hyps R P pcon (D a) xs
hyps R P pcon (`δ A i D) (f , xs) = (λ a ind R P pcon (i a) (i a) (f a))
, hyps R P pcon (D (λ a ode R (i a) (i a) (f a))) xs
----------------------------------------------------------------------
open import Data.Unit
open import Data.Product
module _ where
----------------------------------------------------------------------
data Desc (I : Set) (O : I Set) : Set₁ where
: (i : I) (o : O i) Desc I O
: (A : Set) (i : A I) (D : (o : (a : A) O (i a)) Desc I O) Desc I O
: (A : Set) (D : A Desc I O) Desc I O
⟦_⟧ : {I O} (D : Desc I O) (X : I I Set) (Y : (i j : I) X i j O j) Set
⟦ `ι i o ⟧ X Y =
⟦ `δ A i D ⟧ X Y = Σ ((a : A) X (i a) (i a)) λ f ⟦ D (λ a Y (i a) (i a) (f a)) ⟧ X Y
⟦ `σ A D ⟧ X Y = Σ A λ a ⟦ D a ⟧ X Y
io : {I O} (D : Desc I O) (X : I I Set) (Y : (i j : I) X i j O j) (xs : ⟦ D ⟧ X Y) Σ I O
io (`ι i o) X Y tt = i , o
io (`δ A i D) X Y (f , xs) = io (D (λ a Y (i a) (i a) (f a))) X Y xs
io (`σ A D) X Y (a , xs) = io (D a) X Y xs
{-# TERMINATING #-}
mutual
data μ {I O} (R : I Desc I O) (i : I) : I Set where
init : (xs : ⟦ R i ⟧ (μ R) (ode R)) μ R i (proj₁ (io (R i) (μ R) (ode R) xs))
ode : {I O} (R : I Desc I O) (i j : I) μ R i j O j
ode R i ._ (init xs) = proj₂ (io (R i) (μ R) (ode R) xs)
----------------------------------------------------------------------
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.