Chapter2.Logic

module Chapter2.Logic where

open import Level

open import Data.Unit

infixr 5 _⇒_

Pow : ∀{ℓ} → Set ℓ → Set (suc ℓ)
Pow {ℓ} I = I → Set ℓ

_⇒_ : ∀{ℓ}{I : Set ℓ} → (P Q : Pow I) → Set ℓ
P ⇒ Q = {i : _} → P i → Q i

data _⁻¹_ {ℓ : Level}{A B : Set ℓ}(f : A → B) : Pow B where
  inv : (a : A) → f ⁻¹ (f a)


T : ∀{ℓ}{I : Set ℓ} → I → Set ℓ
T _ = Lift ⊤