module Logic.Logic where



open import Data.Unit

infixr  _⇒_

Pow : Set → Set₁
Pow I = I → Set

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

-- Paper: Remark 4.2
data _⁻¹_ {A B : Set}(f : A → B) : Pow B where
  inv : (a : A) → f ⁻¹ (f a)