postulate A : Set
postulate _≤_ : A → A → Set
postulate refl : {a₀ : A} → a₀ ≤ a₀
postulate trans : {a₀ a₁ a₂ : A} → a₀ ≤ a₁ → a₁ ≤ a₂ → a₀ ≤ a₂


⟦_⟧ : A → Set
⟦_⟧ = {!!}
⇒ : {a₀ a₁ : A} → a₀ ≤ a₁ → ⟦ a₀ ⟧ → ⟦ a₁ ⟧
⇒ = {!!}
⇐ : {a₀ a₁ : A} → (⟦ a₀ ⟧ → ⟦ a₁ ⟧) → a₀ ≤ a₁
⇐ = {!!}