module Prelude.InferenceRules where

open import Prelude.Init

-- syntax for inference rules (separating hypotheses from conclusion)
infix -50
  _──────────────────────────────────────────────────────────────────────────────────────────────────────────────────_
  _─────────────────────────────────────────────────────────────────────────────────────────────────────────────────_
  _────────────────────────────────────────────────────────────────────────────────────────────────────────────────_
  _───────────────────────────────────────────────────────────────────────────────────────────────────────────────_
  _──────────────────────────────────────────────────────────────────────────────────────────────────────────────_
  _─────────────────────────────────────────────────────────────────────────────────────────────────────────────_
  _────────────────────────────────────────────────────────────────────────────────────────────────────────────_
  _───────────────────────────────────────────────────────────────────────────────────────────────────────────_
  _──────────────────────────────────────────────────────────────────────────────────────────────────────────_
  _─────────────────────────────────────────────────────────────────────────────────────────────────────────_
  _────────────────────────────────────────────────────────────────────────────────────────────────────────_
  _───────────────────────────────────────────────────────────────────────────────────────────────────────_
  _──────────────────────────────────────────────────────────────────────────────────────────────────────_
  _─────────────────────────────────────────────────────────────────────────────────────────────────────_
  _────────────────────────────────────────────────────────────────────────────────────────────────────_
  _───────────────────────────────────────────────────────────────────────────────────────────────────_
  _──────────────────────────────────────────────────────────────────────────────────────────────────_
  _─────────────────────────────────────────────────────────────────────────────────────────────────_
  _────────────────────────────────────────────────────────────────────────────────────────────────_
  _───────────────────────────────────────────────────────────────────────────────────────────────_
  _──────────────────────────────────────────────────────────────────────────────────────────────_
  _─────────────────────────────────────────────────────────────────────────────────────────────_
  _────────────────────────────────────────────────────────────────────────────────────────────_
  _───────────────────────────────────────────────────────────────────────────────────────────_
  _──────────────────────────────────────────────────────────────────────────────────────────_
  _─────────────────────────────────────────────────────────────────────────────────────────_
  _────────────────────────────────────────────────────────────────────────────────────────_
  _───────────────────────────────────────────────────────────────────────────────────────_
  _──────────────────────────────────────────────────────────────────────────────────────_
  _─────────────────────────────────────────────────────────────────────────────────────_
  _────────────────────────────────────────────────────────────────────────────────────_
  _───────────────────────────────────────────────────────────────────────────────────_
  _──────────────────────────────────────────────────────────────────────────────────_
  _─────────────────────────────────────────────────────────────────────────────────_
  _────────────────────────────────────────────────────────────────────────────────_
  _───────────────────────────────────────────────────────────────────────────────_
  _──────────────────────────────────────────────────────────────────────────────_
  _─────────────────────────────────────────────────────────────────────────────_
  _────────────────────────────────────────────────────────────────────────────_
  _───────────────────────────────────────────────────────────────────────────_
  _──────────────────────────────────────────────────────────────────────────_
  _─────────────────────────────────────────────────────────────────────────_
  _────────────────────────────────────────────────────────────────────────_
  _───────────────────────────────────────────────────────────────────────_
  _──────────────────────────────────────────────────────────────────────_
  _─────────────────────────────────────────────────────────────────────_
  _────────────────────────────────────────────────────────────────────_
  _───────────────────────────────────────────────────────────────────_
  _──────────────────────────────────────────────────────────────────_
  _─────────────────────────────────────────────────────────────────_
  _────────────────────────────────────────────────────────────────_
  _───────────────────────────────────────────────────────────────_
  _──────────────────────────────────────────────────────────────_
  _─────────────────────────────────────────────────────────────_
  _────────────────────────────────────────────────────────────_
  _───────────────────────────────────────────────────────────_
  _──────────────────────────────────────────────────────────_
  _─────────────────────────────────────────────────────────_
  _────────────────────────────────────────────────────────_
  _───────────────────────────────────────────────────────_
  _──────────────────────────────────────────────────────_
  _─────────────────────────────────────────────────────_
  _────────────────────────────────────────────────────_
  _───────────────────────────────────────────────────_
  _──────────────────────────────────────────────────_
  _─────────────────────────────────────────────────_
  _────────────────────────────────────────────────_
  _───────────────────────────────────────────────_
  _──────────────────────────────────────────────_
  _─────────────────────────────────────────────_
  _────────────────────────────────────────────_
  _───────────────────────────────────────────_
  _──────────────────────────────────────────_
  _─────────────────────────────────────────_
  _────────────────────────────────────────_
  _───────────────────────────────────────_
  _──────────────────────────────────────_
  _─────────────────────────────────────_
  _────────────────────────────────────_
  _───────────────────────────────────_
  _──────────────────────────────────_
  _─────────────────────────────────_
  _────────────────────────────────_
  _───────────────────────────────_
  _──────────────────────────────_
  _─────────────────────────────_
  _────────────────────────────_
  _───────────────────────────_
  _──────────────────────────_
  _─────────────────────────_
  _────────────────────────_
  _───────────────────────_
  _──────────────────────_
  _─────────────────────_
  _────────────────────_
  _───────────────────_
  _──────────────────_
  _─────────────────_
  _────────────────_
  _───────────────_
  _──────────────_
  _─────────────_
  _────────────_
  _───────────_
  _──────────_
  _─────────_
  _────────_
  _───────_
  _──────_
  _─────_
  _────_
  _───_
_──────────────────────────────────────────────────────────────────────────────────────────────────────────────────_
  _─────────────────────────────────────────────────────────────────────────────────────────────────────────────────_
  _────────────────────────────────────────────────────────────────────────────────────────────────────────────────_
  _───────────────────────────────────────────────────────────────────────────────────────────────────────────────_
  _──────────────────────────────────────────────────────────────────────────────────────────────────────────────_
  _─────────────────────────────────────────────────────────────────────────────────────────────────────────────_
  _────────────────────────────────────────────────────────────────────────────────────────────────────────────_
  _───────────────────────────────────────────────────────────────────────────────────────────────────────────_
  _──────────────────────────────────────────────────────────────────────────────────────────────────────────_
  _─────────────────────────────────────────────────────────────────────────────────────────────────────────_
  _────────────────────────────────────────────────────────────────────────────────────────────────────────_
  _───────────────────────────────────────────────────────────────────────────────────────────────────────_
  _──────────────────────────────────────────────────────────────────────────────────────────────────────_
  _─────────────────────────────────────────────────────────────────────────────────────────────────────_
  _────────────────────────────────────────────────────────────────────────────────────────────────────_
  _───────────────────────────────────────────────────────────────────────────────────────────────────_
  _──────────────────────────────────────────────────────────────────────────────────────────────────_
  _─────────────────────────────────────────────────────────────────────────────────────────────────_
  _────────────────────────────────────────────────────────────────────────────────────────────────_
  _───────────────────────────────────────────────────────────────────────────────────────────────_
  _──────────────────────────────────────────────────────────────────────────────────────────────_
  _─────────────────────────────────────────────────────────────────────────────────────────────_
  _────────────────────────────────────────────────────────────────────────────────────────────_
  _───────────────────────────────────────────────────────────────────────────────────────────_
  _──────────────────────────────────────────────────────────────────────────────────────────_
  _─────────────────────────────────────────────────────────────────────────────────────────_
  _────────────────────────────────────────────────────────────────────────────────────────_
  _───────────────────────────────────────────────────────────────────────────────────────_
  _──────────────────────────────────────────────────────────────────────────────────────_
  _─────────────────────────────────────────────────────────────────────────────────────_
  _────────────────────────────────────────────────────────────────────────────────────_
  _───────────────────────────────────────────────────────────────────────────────────_
  _──────────────────────────────────────────────────────────────────────────────────_
  _─────────────────────────────────────────────────────────────────────────────────_
  _────────────────────────────────────────────────────────────────────────────────_
  _───────────────────────────────────────────────────────────────────────────────_
  _──────────────────────────────────────────────────────────────────────────────_
  _─────────────────────────────────────────────────────────────────────────────_
  _────────────────────────────────────────────────────────────────────────────_
  _───────────────────────────────────────────────────────────────────────────_
  _──────────────────────────────────────────────────────────────────────────_
  _─────────────────────────────────────────────────────────────────────────_
  _────────────────────────────────────────────────────────────────────────_
  _───────────────────────────────────────────────────────────────────────_
  _──────────────────────────────────────────────────────────────────────_
  _─────────────────────────────────────────────────────────────────────_
  _────────────────────────────────────────────────────────────────────_
  _───────────────────────────────────────────────────────────────────_
  _──────────────────────────────────────────────────────────────────_
  _─────────────────────────────────────────────────────────────────_
  _────────────────────────────────────────────────────────────────_
  _───────────────────────────────────────────────────────────────_
  _──────────────────────────────────────────────────────────────_
  _─────────────────────────────────────────────────────────────_
  _────────────────────────────────────────────────────────────_
  _───────────────────────────────────────────────────────────_
  _──────────────────────────────────────────────────────────_
  _─────────────────────────────────────────────────────────_
  _────────────────────────────────────────────────────────_
  _───────────────────────────────────────────────────────_
  _──────────────────────────────────────────────────────_
  _─────────────────────────────────────────────────────_
  _────────────────────────────────────────────────────_
  _───────────────────────────────────────────────────_
  _──────────────────────────────────────────────────_
  _─────────────────────────────────────────────────_
  _────────────────────────────────────────────────_
  _───────────────────────────────────────────────_
  _──────────────────────────────────────────────_
  _─────────────────────────────────────────────_
  _────────────────────────────────────────────_
  _───────────────────────────────────────────_
  _──────────────────────────────────────────_
  _─────────────────────────────────────────_
  _────────────────────────────────────────_
  _───────────────────────────────────────_
  _──────────────────────────────────────_
  _─────────────────────────────────────_
  _────────────────────────────────────_
  _───────────────────────────────────_
  _──────────────────────────────────_
  _─────────────────────────────────_
  _────────────────────────────────_
  _───────────────────────────────_
  _──────────────────────────────_
  _─────────────────────────────_
  _────────────────────────────_
  _───────────────────────────_
  _──────────────────────────_
  _─────────────────────────_
  _────────────────────────_
  _───────────────────────_
  _──────────────────────_
  _─────────────────────_
  _────────────────────_
  _───────────────────_
  _──────────────────_
  _─────────────────_
  _────────────────_
  _───────────────_
  _──────────────_
  _─────────────_
  _────────────_
  _───────────_
  _──────────_
  _─────────_
  _────────_
  _───────_
  _──────_
  _─────_
  _────_
  _───_
  : Set ℓ → Set ℓ′ → Set (ℓ ⊔ₗ ℓ′)
A ────────────────────────────────────────────────────────────────────────────────────────────────────────────────── B = A → B
A  ───────────────────────────────────────────────────────────────────────────────────────────────────────────────── B = A → B
A   ──────────────────────────────────────────────────────────────────────────────────────────────────────────────── B = A → B
A    ─────────────────────────────────────────────────────────────────────────────────────────────────────────────── B = A → B
A     ────────────────────────────────────────────────────────────────────────────────────────────────────────────── B = A → B
A      ───────────────────────────────────────────────────────────────────────────────────────────────────────────── B = A → B
A       ──────────────────────────────────────────────────────────────────────────────────────────────────────────── B = A → B
A        ─────────────────────────────────────────────────────────────────────────────────────────────────────────── B = A → B
A         ────────────────────────────────────────────────────────────────────────────────────────────────────────── B = A → B
A          ───────────────────────────────────────────────────────────────────────────────────────────────────────── B = A → B
A           ──────────────────────────────────────────────────────────────────────────────────────────────────────── B = A → B
A            ─────────────────────────────────────────────────────────────────────────────────────────────────────── B = A → B
A             ────────────────────────────────────────────────────────────────────────────────────────────────────── B = A → B
A              ───────────────────────────────────────────────────────────────────────────────────────────────────── B = A → B
A               ──────────────────────────────────────────────────────────────────────────────────────────────────── B = A → B
A                ─────────────────────────────────────────────────────────────────────────────────────────────────── B = A → B
A                 ────────────────────────────────────────────────────────────────────────────────────────────────── B = A → B
A                  ───────────────────────────────────────────────────────────────────────────────────────────────── B = A → B
A                   ──────────────────────────────────────────────────────────────────────────────────────────────── B = A → B
A                    ─────────────────────────────────────────────────────────────────────────────────────────────── B = A → B
A                     ────────────────────────────────────────────────────────────────────────────────────────────── B = A → B
A                      ───────────────────────────────────────────────────────────────────────────────────────────── B = A → B
A                       ──────────────────────────────────────────────────────────────────────────────────────────── B = A → B
A                        ─────────────────────────────────────────────────────────────────────────────────────────── B = A → B
A                         ────────────────────────────────────────────────────────────────────────────────────────── B = A → B
A                          ───────────────────────────────────────────────────────────────────────────────────────── B = A → B
A                           ──────────────────────────────────────────────────────────────────────────────────────── B = A → B
A                            ─────────────────────────────────────────────────────────────────────────────────────── B = A → B
A                             ────────────────────────────────────────────────────────────────────────────────────── B = A → B
A                              ───────────────────────────────────────────────────────────────────────────────────── B = A → B
A                               ──────────────────────────────────────────────────────────────────────────────────── B = A → B
A                                ─────────────────────────────────────────────────────────────────────────────────── B = A → B
A                                 ────────────────────────────────────────────────────────────────────────────────── B = A → B
A                                  ───────────────────────────────────────────────────────────────────────────────── B = A → B
A                                   ──────────────────────────────────────────────────────────────────────────────── B = A → B
A                                    ─────────────────────────────────────────────────────────────────────────────── B = A → B
A                                     ────────────────────────────────────────────────────────────────────────────── B = A → B
A                                      ───────────────────────────────────────────────────────────────────────────── B = A → B
A                                       ──────────────────────────────────────────────────────────────────────────── B = A → B
A                                        ─────────────────────────────────────────────────────────────────────────── B = A → B
A                                         ────────────────────────────────────────────────────────────────────────── B = A → B
A                                          ───────────────────────────────────────────────────────────────────────── B = A → B
A                                           ──────────────────────────────────────────────────────────────────────── B = A → B
A                                            ─────────────────────────────────────────────────────────────────────── B = A → B
A                                             ────────────────────────────────────────────────────────────────────── B = A → B
A                                              ───────────────────────────────────────────────────────────────────── B = A → B
A                                               ──────────────────────────────────────────────────────────────────── B = A → B
A                                                ─────────────────────────────────────────────────────────────────── B = A → B
A                                                 ────────────────────────────────────────────────────────────────── B = A → B
A                                                  ───────────────────────────────────────────────────────────────── B = A → B
A                                                   ──────────────────────────────────────────────────────────────── B = A → B
A                                                    ─────────────────────────────────────────────────────────────── B = A → B
A                                                     ────────────────────────────────────────────────────────────── B = A → B
A                                                      ───────────────────────────────────────────────────────────── B = A → B
A                                                       ──────────────────────────────────────────────────────────── B = A → B
A                                                        ─────────────────────────────────────────────────────────── B = A → B
A                                                         ────────────────────────────────────────────────────────── B = A → B
A                                                          ───────────────────────────────────────────────────────── B = A → B
A                                                           ──────────────────────────────────────────────────────── B = A → B
A                                                            ─────────────────────────────────────────────────────── B = A → B
A                                                             ────────────────────────────────────────────────────── B = A → B
A                                                              ───────────────────────────────────────────────────── B = A → B
A                                                               ──────────────────────────────────────────────────── B = A → B
A                                                                ─────────────────────────────────────────────────── B = A → B
A                                                                 ────────────────────────────────────────────────── B = A → B
A                                                                  ───────────────────────────────────────────────── B = A → B
A                                                                   ──────────────────────────────────────────────── B = A → B
A                                                                    ─────────────────────────────────────────────── B = A → B
A                                                                     ────────────────────────────────────────────── B = A → B
A                                                                      ───────────────────────────────────────────── B = A → B
A                                                                       ──────────────────────────────────────────── B = A → B
A                                                                        ─────────────────────────────────────────── B = A → B
A                                                                         ────────────────────────────────────────── B = A → B
A                                                                          ───────────────────────────────────────── B = A → B
A                                                                           ──────────────────────────────────────── B = A → B
A                                                                            ─────────────────────────────────────── B = A → B
A                                                                             ────────────────────────────────────── B = A → B
A                                                                              ───────────────────────────────────── B = A → B
A                                                                               ──────────────────────────────────── B = A → B
A                                                                                ─────────────────────────────────── B = A → B
A                                                                                 ────────────────────────────────── B = A → B
A                                                                                  ───────────────────────────────── B = A → B
A                                                                                   ──────────────────────────────── B = A → B
A                                                                                    ─────────────────────────────── B = A → B
A                                                                                     ────────────────────────────── B = A → B
A                                                                                      ───────────────────────────── B = A → B
A                                                                                       ──────────────────────────── B = A → B
A                                                                                        ─────────────────────────── B = A → B
A                                                                                         ────────────────────────── B = A → B
A                                                                                          ───────────────────────── B = A → B
A                                                                                           ──────────────────────── B = A → B
A                                                                                            ─────────────────────── B = A → B
A                                                                                             ────────────────────── B = A → B
A                                                                                              ───────────────────── B = A → B
A                                                                                               ──────────────────── B = A → B
A                                                                                                ─────────────────── B = A → B
A                                                                                                 ────────────────── B = A → B
A                                                                                                  ───────────────── B = A → B
A                                                                                                   ──────────────── B = A → B
A                                                                                                    ─────────────── B = A → B
A                                                                                                     ────────────── B = A → B
A                                                                                                      ───────────── B = A → B
A                                                                                                       ──────────── B = A → B
A                                                                                                        ─────────── B = A → B
A                                                                                                         ────────── B = A → B
A                                                                                                          ───────── B = A → B
A                                                                                                           ──────── B = A → B
A                                                                                                            ─────── B = A → B
A                                                                                                             ────── B = A → B
A                                                                                                              ───── B = A → B
A                                                                                                               ──── B = A → B
A                                                                                                                ─── B = A → B

infix -100
  ──────────────────────────────────────────────────────────────────────────────────────────────────────────────────_
  ─────────────────────────────────────────────────────────────────────────────────────────────────────────────────_
  ────────────────────────────────────────────────────────────────────────────────────────────────────────────────_
  ───────────────────────────────────────────────────────────────────────────────────────────────────────────────_
  ──────────────────────────────────────────────────────────────────────────────────────────────────────────────_
  ─────────────────────────────────────────────────────────────────────────────────────────────────────────────_
  ────────────────────────────────────────────────────────────────────────────────────────────────────────────_
  ───────────────────────────────────────────────────────────────────────────────────────────────────────────_
  ──────────────────────────────────────────────────────────────────────────────────────────────────────────_
  ─────────────────────────────────────────────────────────────────────────────────────────────────────────_
  ────────────────────────────────────────────────────────────────────────────────────────────────────────_
  ───────────────────────────────────────────────────────────────────────────────────────────────────────_
  ──────────────────────────────────────────────────────────────────────────────────────────────────────_
  ─────────────────────────────────────────────────────────────────────────────────────────────────────_
  ────────────────────────────────────────────────────────────────────────────────────────────────────_
  ───────────────────────────────────────────────────────────────────────────────────────────────────_
  ──────────────────────────────────────────────────────────────────────────────────────────────────_
  ─────────────────────────────────────────────────────────────────────────────────────────────────_
  ────────────────────────────────────────────────────────────────────────────────────────────────_
  ───────────────────────────────────────────────────────────────────────────────────────────────_
  ──────────────────────────────────────────────────────────────────────────────────────────────_
  ─────────────────────────────────────────────────────────────────────────────────────────────_
  ────────────────────────────────────────────────────────────────────────────────────────────_
  ───────────────────────────────────────────────────────────────────────────────────────────_
  ──────────────────────────────────────────────────────────────────────────────────────────_
  ─────────────────────────────────────────────────────────────────────────────────────────_
  ────────────────────────────────────────────────────────────────────────────────────────_
  ───────────────────────────────────────────────────────────────────────────────────────_
  ──────────────────────────────────────────────────────────────────────────────────────_
  ─────────────────────────────────────────────────────────────────────────────────────_
  ────────────────────────────────────────────────────────────────────────────────────_
  ───────────────────────────────────────────────────────────────────────────────────_
  ──────────────────────────────────────────────────────────────────────────────────_
  ─────────────────────────────────────────────────────────────────────────────────_
  ────────────────────────────────────────────────────────────────────────────────_
  ───────────────────────────────────────────────────────────────────────────────_
  ──────────────────────────────────────────────────────────────────────────────_
  ─────────────────────────────────────────────────────────────────────────────_
  ────────────────────────────────────────────────────────────────────────────_
  ───────────────────────────────────────────────────────────────────────────_
  ──────────────────────────────────────────────────────────────────────────_
  ─────────────────────────────────────────────────────────────────────────_
  ────────────────────────────────────────────────────────────────────────_
  ───────────────────────────────────────────────────────────────────────_
  ──────────────────────────────────────────────────────────────────────_
  ─────────────────────────────────────────────────────────────────────_
  ────────────────────────────────────────────────────────────────────_
  ───────────────────────────────────────────────────────────────────_
  ──────────────────────────────────────────────────────────────────_
  ─────────────────────────────────────────────────────────────────_
  ────────────────────────────────────────────────────────────────_
  ───────────────────────────────────────────────────────────────_
  ──────────────────────────────────────────────────────────────_
  ─────────────────────────────────────────────────────────────_
  ────────────────────────────────────────────────────────────_
  ───────────────────────────────────────────────────────────_
  ──────────────────────────────────────────────────────────_
  ─────────────────────────────────────────────────────────_
  ────────────────────────────────────────────────────────_
  ───────────────────────────────────────────────────────_
  ──────────────────────────────────────────────────────_
  ─────────────────────────────────────────────────────_
  ────────────────────────────────────────────────────_
  ───────────────────────────────────────────────────_
  ──────────────────────────────────────────────────_
  ─────────────────────────────────────────────────_
  ────────────────────────────────────────────────_
  ───────────────────────────────────────────────_
  ──────────────────────────────────────────────_
  ─────────────────────────────────────────────_
  ────────────────────────────────────────────_
  ───────────────────────────────────────────_
  ──────────────────────────────────────────_
  ─────────────────────────────────────────_
  ────────────────────────────────────────_
  ───────────────────────────────────────_
  ──────────────────────────────────────_
  ─────────────────────────────────────_
  ────────────────────────────────────_
  ───────────────────────────────────_
  ──────────────────────────────────_
  ─────────────────────────────────_
  ────────────────────────────────_
  ───────────────────────────────_
  ──────────────────────────────_
  ─────────────────────────────_
  ────────────────────────────_
  ───────────────────────────_
  ──────────────────────────_
  ─────────────────────────_
  ────────────────────────_
  ───────────────────────_
  ──────────────────────_
  ─────────────────────_
  ────────────────────_
  ───────────────────_
  ──────────────────_
  ─────────────────_
  ────────────────_
  ───────────────_
  ──────────────_
  ─────────────_
  ────────────_
  ───────────_
  ──────────_
  ─────────_
  ────────_
  ───────_
  ──────_
  ─────_
  ────_
  ───_
──────────────────────────────────────────────────────────────────────────────────────────────────────────────────_
 ─────────────────────────────────────────────────────────────────────────────────────────────────────────────────_
  ────────────────────────────────────────────────────────────────────────────────────────────────────────────────_
   ───────────────────────────────────────────────────────────────────────────────────────────────────────────────_
    ──────────────────────────────────────────────────────────────────────────────────────────────────────────────_
     ─────────────────────────────────────────────────────────────────────────────────────────────────────────────_
      ────────────────────────────────────────────────────────────────────────────────────────────────────────────_
       ───────────────────────────────────────────────────────────────────────────────────────────────────────────_
        ──────────────────────────────────────────────────────────────────────────────────────────────────────────_
         ─────────────────────────────────────────────────────────────────────────────────────────────────────────_
          ────────────────────────────────────────────────────────────────────────────────────────────────────────_
           ───────────────────────────────────────────────────────────────────────────────────────────────────────_
            ──────────────────────────────────────────────────────────────────────────────────────────────────────_
             ─────────────────────────────────────────────────────────────────────────────────────────────────────_
              ────────────────────────────────────────────────────────────────────────────────────────────────────_
               ───────────────────────────────────────────────────────────────────────────────────────────────────_
                ──────────────────────────────────────────────────────────────────────────────────────────────────_
                 ─────────────────────────────────────────────────────────────────────────────────────────────────_
                  ────────────────────────────────────────────────────────────────────────────────────────────────_
                   ───────────────────────────────────────────────────────────────────────────────────────────────_
                    ──────────────────────────────────────────────────────────────────────────────────────────────_
                     ─────────────────────────────────────────────────────────────────────────────────────────────_
                      ────────────────────────────────────────────────────────────────────────────────────────────_
                       ───────────────────────────────────────────────────────────────────────────────────────────_
                        ──────────────────────────────────────────────────────────────────────────────────────────_
                         ─────────────────────────────────────────────────────────────────────────────────────────_
                          ────────────────────────────────────────────────────────────────────────────────────────_
                           ───────────────────────────────────────────────────────────────────────────────────────_
                            ──────────────────────────────────────────────────────────────────────────────────────_
                             ─────────────────────────────────────────────────────────────────────────────────────_
                              ────────────────────────────────────────────────────────────────────────────────────_
                               ───────────────────────────────────────────────────────────────────────────────────_
                                ──────────────────────────────────────────────────────────────────────────────────_
                                 ─────────────────────────────────────────────────────────────────────────────────_
                                  ────────────────────────────────────────────────────────────────────────────────_
                                   ───────────────────────────────────────────────────────────────────────────────_
                                    ──────────────────────────────────────────────────────────────────────────────_
                                     ─────────────────────────────────────────────────────────────────────────────_
                                      ────────────────────────────────────────────────────────────────────────────_
                                       ───────────────────────────────────────────────────────────────────────────_
                                        ──────────────────────────────────────────────────────────────────────────_
                                         ─────────────────────────────────────────────────────────────────────────_
                                          ────────────────────────────────────────────────────────────────────────_
                                           ───────────────────────────────────────────────────────────────────────_
                                            ──────────────────────────────────────────────────────────────────────_
                                             ─────────────────────────────────────────────────────────────────────_
                                              ────────────────────────────────────────────────────────────────────_
                                               ───────────────────────────────────────────────────────────────────_
                                                ──────────────────────────────────────────────────────────────────_
                                                 ─────────────────────────────────────────────────────────────────_
                                                  ────────────────────────────────────────────────────────────────_
                                                   ───────────────────────────────────────────────────────────────_
                                                    ──────────────────────────────────────────────────────────────_
                                                     ─────────────────────────────────────────────────────────────_
                                                      ────────────────────────────────────────────────────────────_
                                                       ───────────────────────────────────────────────────────────_
                                                        ──────────────────────────────────────────────────────────_
                                                         ─────────────────────────────────────────────────────────_
                                                          ────────────────────────────────────────────────────────_
                                                           ───────────────────────────────────────────────────────_
                                                            ──────────────────────────────────────────────────────_
                                                             ─────────────────────────────────────────────────────_
                                                              ────────────────────────────────────────────────────_
                                                               ───────────────────────────────────────────────────_
                                                                ──────────────────────────────────────────────────_
                                                                 ─────────────────────────────────────────────────_
                                                                  ────────────────────────────────────────────────_
                                                                   ───────────────────────────────────────────────_
                                                                    ──────────────────────────────────────────────_
                                                                     ─────────────────────────────────────────────_
                                                                      ────────────────────────────────────────────_
                                                                       ───────────────────────────────────────────_
                                                                        ──────────────────────────────────────────_
                                                                         ─────────────────────────────────────────_
                                                                          ────────────────────────────────────────_
                                                                           ───────────────────────────────────────_
                                                                            ──────────────────────────────────────_
                                                                             ─────────────────────────────────────_
                                                                              ────────────────────────────────────_
                                                                               ───────────────────────────────────_
                                                                                ──────────────────────────────────_
                                                                                 ─────────────────────────────────_
                                                                                  ────────────────────────────────_
                                                                                   ───────────────────────────────_
                                                                                    ──────────────────────────────_
                                                                                     ─────────────────────────────_
                                                                                      ────────────────────────────_
                                                                                       ───────────────────────────_
                                                                                        ──────────────────────────_
                                                                                         ─────────────────────────_
                                                                                          ────────────────────────_
                                                                                           ───────────────────────_
                                                                                            ──────────────────────_
                                                                                             ─────────────────────_
                                                                                              ────────────────────_
                                                                                               ───────────────────_
                                                                                                ──────────────────_
                                                                                                 ─────────────────_
                                                                                                  ────────────────_
                                                                                                   ───────────────_
                                                                                                    ──────────────_
                                                                                                     ─────────────_
                                                                                                      ────────────_
                                                                                                       ───────────_
                                                                                                        ──────────_
                                                                                                         ─────────_
                                                                                                          ────────_
                                                                                                           ───────_
                                                                                                            ──────_
                                                                                                             ─────_
                                                                                                              ────_
                                                                                                               ───_
  : Set ℓ → Set ℓ
────────────────────────────────────────────────────────────────────────────────────────────────────────────────── A = A
───────────────────────────────────────────────────────────────────────────────────────────────────────────────── A = A
──────────────────────────────────────────────────────────────────────────────────────────────────────────────── A = A
─────────────────────────────────────────────────────────────────────────────────────────────────────────────── A = A
────────────────────────────────────────────────────────────────────────────────────────────────────────────── A = A
───────────────────────────────────────────────────────────────────────────────────────────────────────────── A = A
──────────────────────────────────────────────────────────────────────────────────────────────────────────── A = A
─────────────────────────────────────────────────────────────────────────────────────────────────────────── A = A
────────────────────────────────────────────────────────────────────────────────────────────────────────── A = A
───────────────────────────────────────────────────────────────────────────────────────────────────────── A = A
──────────────────────────────────────────────────────────────────────────────────────────────────────── A = A
─────────────────────────────────────────────────────────────────────────────────────────────────────── A = A
────────────────────────────────────────────────────────────────────────────────────────────────────── A = A
───────────────────────────────────────────────────────────────────────────────────────────────────── A = A
──────────────────────────────────────────────────────────────────────────────────────────────────── A = A
─────────────────────────────────────────────────────────────────────────────────────────────────── A = A
────────────────────────────────────────────────────────────────────────────────────────────────── A = A
───────────────────────────────────────────────────────────────────────────────────────────────── A = A
──────────────────────────────────────────────────────────────────────────────────────────────── A = A
─────────────────────────────────────────────────────────────────────────────────────────────── A = A
────────────────────────────────────────────────────────────────────────────────────────────── A = A
───────────────────────────────────────────────────────────────────────────────────────────── A = A
──────────────────────────────────────────────────────────────────────────────────────────── A = A
─────────────────────────────────────────────────────────────────────────────────────────── A = A
────────────────────────────────────────────────────────────────────────────────────────── A = A
───────────────────────────────────────────────────────────────────────────────────────── A = A
──────────────────────────────────────────────────────────────────────────────────────── A = A
─────────────────────────────────────────────────────────────────────────────────────── A = A
────────────────────────────────────────────────────────────────────────────────────── A = A
───────────────────────────────────────────────────────────────────────────────────── A = A
──────────────────────────────────────────────────────────────────────────────────── A = A
─────────────────────────────────────────────────────────────────────────────────── A = A
────────────────────────────────────────────────────────────────────────────────── A = A
───────────────────────────────────────────────────────────────────────────────── A = A
──────────────────────────────────────────────────────────────────────────────── A = A
─────────────────────────────────────────────────────────────────────────────── A = A
────────────────────────────────────────────────────────────────────────────── A = A
───────────────────────────────────────────────────────────────────────────── A = A
──────────────────────────────────────────────────────────────────────────── A = A
─────────────────────────────────────────────────────────────────────────── A = A
────────────────────────────────────────────────────────────────────────── A = A
───────────────────────────────────────────────────────────────────────── A = A
──────────────────────────────────────────────────────────────────────── A = A
─────────────────────────────────────────────────────────────────────── A = A
────────────────────────────────────────────────────────────────────── A = A
───────────────────────────────────────────────────────────────────── A = A
──────────────────────────────────────────────────────────────────── A = A
─────────────────────────────────────────────────────────────────── A = A
────────────────────────────────────────────────────────────────── A = A
───────────────────────────────────────────────────────────────── A = A
──────────────────────────────────────────────────────────────── A = A
─────────────────────────────────────────────────────────────── A = A
────────────────────────────────────────────────────────────── A = A
───────────────────────────────────────────────────────────── A = A
──────────────────────────────────────────────────────────── A = A
─────────────────────────────────────────────────────────── A = A
────────────────────────────────────────────────────────── A = A
───────────────────────────────────────────────────────── A = A
──────────────────────────────────────────────────────── A = A
─────────────────────────────────────────────────────── A = A
────────────────────────────────────────────────────── A = A
───────────────────────────────────────────────────── A = A
──────────────────────────────────────────────────── A = A
─────────────────────────────────────────────────── A = A
────────────────────────────────────────────────── A = A
───────────────────────────────────────────────── A = A
──────────────────────────────────────────────── A = A
─────────────────────────────────────────────── A = A
────────────────────────────────────────────── A = A
───────────────────────────────────────────── A = A
──────────────────────────────────────────── A = A
─────────────────────────────────────────── A = A
────────────────────────────────────────── A = A
───────────────────────────────────────── A = A
──────────────────────────────────────── A = A
─────────────────────────────────────── A = A
────────────────────────────────────── A = A
───────────────────────────────────── A = A
──────────────────────────────────── A = A
─────────────────────────────────── A = A
────────────────────────────────── A = A
───────────────────────────────── A = A
──────────────────────────────── A = A
─────────────────────────────── A = A
────────────────────────────── A = A
───────────────────────────── A = A
──────────────────────────── A = A
─────────────────────────── A = A
────────────────────────── A = A
───────────────────────── A = A
──────────────────────── A = A
─────────────────────── A = A
────────────────────── A = A
───────────────────── A = A
──────────────────── A = A
─────────────────── A = A
────────────────── A = A
───────────────── A = A
──────────────── A = A
─────────────── A = A
────────────── A = A
───────────── A = A
──────────── A = A
─────────── A = A
────────── A = A
───────── A = A
──────── A = A
─────── A = A
────── A = A
───── A = A
──── A = A
─── A = A

infixr -100 _∙_
_∙_ : Set ℓ → Set ℓ′ → Set (ℓ ⊔ₗ ℓ′)
A ∙ B = A → B

infix -150 ∙_
∙_ : Set ℓ → Set ℓ
∙ A = A

private
  _ : Set
  _ = ∀ {l : Level} →
    ─────────────────
    l ≡ 0ℓ

  _ : Set
  _ = ∀ {l : Level} →
    ∙ l ≢ 1ℓ
    ∙ l ≢ 2ℓ
    ∙ l ≢ 3ℓ
      ──────
      l ≡ 0ℓ

  _ : Set
  _ = ∀ {l : Level} →
    -- [LIMITATION] cannot have dependent function space, aka Π-types
    -- ∙ (∃x : ∃ (_> l))
    -- ∙ (∃y : ∃ (_≤ l))
    ∀ (∃x : ∃ (_≡ l)) →
    ∙ l ≢ 1ℓ
    → (∃y : ∃ (_≢ l))
    → l ≢ 2ℓ
    ∙ l ≢ 3ℓ
    → let x , _ = ∃x; y , _ = ∃y in
    ∙ x ≢ y
      ─────────────────────────────
      l ≡ 0ℓ

  -- making sure precedence works as expected
  data X : Pred₀ Level where
    ruleX :
      ∙ ℓ ≢ 1ℓ
      ∙ ℓ ≢ 2ℓ
        ───────
        X ℓ
  data Y : Pred₀ Level where
    ruleY :
        ℓ ≢ 1ℓ
      → ℓ ≢ 2ℓ
        --—————
      → Y ℓ

  open import Prelude.General
  X⇔Y : X ℓ ↔ Y ℓ
  X⇔Y = ↝ , ↜
    where
      ↝ = λ where (ruleX p q) → ruleY p q
      ↜ = λ where (ruleY p q) → ruleX p q