open import Level

module Chapter5.IDesc.Algebra.Quantifiers
         { : Level}
         {A B : Set }
         (f : A  B)
       where

open import Chapter2.Logic

open import Chapter5.IDesc

 : func  B A
 = func.mk λ a  `var (f a)

Δ : Pow B  Pow A
Δ =   ⟧func

 : func  A B
 = func.mk λ b   (f ⁻¹ b) help
  where help : ∀{b}  f ⁻¹ b  IDesc  A
        help (inv a) = `var a

Σ : Pow A  Pow B
Σ =   ⟧func

 : func  A B
 = func.mk λ b   (f ⁻¹ b) help
  where help : ∀{b}  f ⁻¹ b  IDesc  A
        help (inv a) = `var a

Π : Pow A  Pow B
Π =   ⟧func