open import Level module Chapter5.IDesc.Algebra.Quantifiers {ℓ : Level} {A B : Set ℓ} (f : A → B) where open import Chapter2.Logic open import Chapter5.IDesc DΔ : func ℓ B A DΔ = func.mk λ a → `var (f a) Δ : Pow B → Pow A Δ = ⟦ DΔ ⟧func DΣ : func ℓ A B DΣ = func.mk λ b → `Σ (f ⁻¹ b) help where help : ∀{b} → f ⁻¹ b → IDesc ℓ A help (inv a) = `var a Σ : Pow A → Pow B Σ = ⟦ DΣ ⟧func DΠ : func ℓ A B DΠ = func.mk λ b → `Π (f ⁻¹ b) help where help : ∀{b} → f ⁻¹ b → IDesc ℓ A help (inv a) = `var a Π : Pow A → Pow B Π = ⟦ DΠ ⟧func