3
module Foo (_ : Set₁) where
7
module FooApp = Foo Set
13
⟦ tt ⟧₁ x = FooApp.Id x
16
fix : ⟦ x ⟧₁ (μ₁ x) -> μ₁ x
19
module Matrices (J : Set) where
21
Id : (J → Set) → J → Set
25
id : (D : Poly) -> Poly
27
module Dim (I : Set) where
30
⟦_⟧₂ : Poly → (I → Set) → (I → Set)
31
⟦ id D ⟧₂ x i = M.Id x i
33
data μ₂ (p : Poly) (i : I) : Set where
34
fix : ⟦ p ⟧₂ (μ₂ p) i -> μ₂ p i