Last active
October 30, 2025 22:29
-
-
Save noughtmare/3fc0dc8b1e9f7dc4c6d0cc0804bc2f2d to your computer and use it in GitHub Desktop.
Induction for descriptions with fixpoints
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| open import Level using (Level) renaming (suc to lsuc ; zero to lzero) | |
| open import Function | |
| open import Data.Sum using (_⊎_ ; inj₁ ; inj₂) | |
| variable ℓ : Level | |
| data Desc (I : Set) : Set₁ where | |
| var : I → Desc I | |
| σ π : (A : Set) (D : A → Desc I) → Desc I | |
| _×D_ : Desc I → Desc I → Desc I | |
| κ : Set → Desc I | |
| μ : (J : Set) → (J → Desc (I ⊎ J)) → J → Desc I | |
| indDesc : (P : (I : Set) → Desc I → Set ℓ) | |
| → ((I : Set) (i : I) → P I (var i)) | |
| → ((I : Set) (A : Set) (D : A → Desc I) → ((x : A) → P I (D x)) → P I (σ A D)) | |
| → ((I : Set) (A : Set) (D : A → Desc I) → ((x : A) → P I (D x)) → P I (π A D)) | |
| → ((I : Set) (x y : Desc I) → P I x → P I y → P I (x ×D y)) | |
| → ((I : Set) (A : Set) → P I (κ A)) | |
| → ((I J : Set) (f : J → Desc (I ⊎ J)) → (j : J) → ((j : J) → P (I ⊎ J) (f j)) → P I (μ J f j)) | |
| → (I : Set) (x : Desc I) → P I x | |
| indDesc P x₀ x₁ x₂ x₃ x₄ x₅ I (var i) = x₀ I i | |
| indDesc P x₀ x₁ x₂ x₃ x₄ x₅ I (σ A D) = x₁ I A D (indDesc P x₀ x₁ x₂ x₃ x₄ x₅ I ∘ D) | |
| indDesc P x₀ x₁ x₂ x₃ x₄ x₅ I (π A D) = x₂ I A D (indDesc P x₀ x₁ x₂ x₃ x₄ x₅ I ∘ D) | |
| indDesc P x₀ x₁ x₂ x₃ x₄ x₅ I (x ×D y) = x₃ I x y (indDesc P x₀ x₁ x₂ x₃ x₄ x₅ I x) (indDesc P x₀ x₁ x₂ x₃ x₄ x₅ I y) | |
| indDesc P x₀ x₁ x₂ x₃ x₄ x₅ I (κ A) = x₄ I A | |
| indDesc P x₀ x₁ x₂ x₃ x₄ x₅ I (μ J f j) = x₅ I J f j (indDesc P x₀ x₁ x₂ x₃ x₄ x₅ (I ⊎ J) ∘ f) | |
| -- sanity check | |
| idDesc : (I : Set) → Desc I → Desc I | |
| idDesc = indDesc (λ I _ → Desc I) (λ _ → var) (λ _ A _ f → σ A f) (λ _ A _ f → π A f) (λ _ _ _ x y → x ×D y) (λ _ A → κ A) (λ _ J _ j f → μ J f j) |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment