{-# OPTIONS --safe #-}
module Prelude.InferenceRules where

open import Prelude.Init

-- syntax for inference rules (separating hypotheses from conclusion)
infix -50
  _──────────────────────────────────────────────────────────────────────────────────────────────────────────────────_
  _─────────────────────────────────────────────────────────────────────────────────────────────────────────────────_
  _────────────────────────────────────────────────────────────────────────────────────────────────────────────────_
  _───────────────────────────────────────────────────────────────────────────────────────────────────────────────_
  _──────────────────────────────────────────────────────────────────────────────────────────────────────────────_
  _─────────────────────────────────────────────────────────────────────────────────────────────────────────────_
  _────────────────────────────────────────────────────────────────────────────────────────────────────────────_
  _───────────────────────────────────────────────────────────────────────────────────────────────────────────_
  _──────────────────────────────────────────────────────────────────────────────────────────────────────────_
  _─────────────────────────────────────────────────────────────────────────────────────────────────────────_
  _────────────────────────────────────────────────────────────────────────────────────────────────────────_
  _───────────────────────────────────────────────────────────────────────────────────────────────────────_
  _──────────────────────────────────────────────────────────────────────────────────────────────────────_
  _─────────────────────────────────────────────────────────────────────────────────────────────────────_
  _────────────────────────────────────────────────────────────────────────────────────────────────────_
  _───────────────────────────────────────────────────────────────────────────────────────────────────_
  _──────────────────────────────────────────────────────────────────────────────────────────────────_
  _─────────────────────────────────────────────────────────────────────────────────────────────────_
  _────────────────────────────────────────────────────────────────────────────────────────────────_
  _───────────────────────────────────────────────────────────────────────────────────────────────_
  _──────────────────────────────────────────────────────────────────────────────────────────────_
  _─────────────────────────────────────────────────────────────────────────────────────────────_
  _────────────────────────────────────────────────────────────────────────────────────────────_
  _───────────────────────────────────────────────────────────────────────────────────────────_
  _──────────────────────────────────────────────────────────────────────────────────────────_
  _─────────────────────────────────────────────────────────────────────────────────────────_
  _────────────────────────────────────────────────────────────────────────────────────────_
  _───────────────────────────────────────────────────────────────────────────────────────_
  _──────────────────────────────────────────────────────────────────────────────────────_
  _─────────────────────────────────────────────────────────────────────────────────────_
  _────────────────────────────────────────────────────────────────────────────────────_
  _───────────────────────────────────────────────────────────────────────────────────_
  _──────────────────────────────────────────────────────────────────────────────────_
  _─────────────────────────────────────────────────────────────────────────────────_
  _────────────────────────────────────────────────────────────────────────────────_
  _───────────────────────────────────────────────────────────────────────────────_
  _──────────────────────────────────────────────────────────────────────────────_
  _─────────────────────────────────────────────────────────────────────────────_
  _────────────────────────────────────────────────────────────────────────────_
  _───────────────────────────────────────────────────────────────────────────_
  _──────────────────────────────────────────────────────────────────────────_
  _─────────────────────────────────────────────────────────────────────────_
  _────────────────────────────────────────────────────────────────────────_
  _───────────────────────────────────────────────────────────────────────_
  _──────────────────────────────────────────────────────────────────────_
  _─────────────────────────────────────────────────────────────────────_
  _────────────────────────────────────────────────────────────────────_
  _───────────────────────────────────────────────────────────────────_
  _──────────────────────────────────────────────────────────────────_
  _─────────────────────────────────────────────────────────────────_
  _────────────────────────────────────────────────────────────────_
  _───────────────────────────────────────────────────────────────_
  _──────────────────────────────────────────────────────────────_
  _─────────────────────────────────────────────────────────────_
  _────────────────────────────────────────────────────────────_
  _───────────────────────────────────────────────────────────_
  _──────────────────────────────────────────────────────────_
  _─────────────────────────────────────────────────────────_
  _────────────────────────────────────────────────────────_
  _───────────────────────────────────────────────────────_
  _──────────────────────────────────────────────────────_
  _─────────────────────────────────────────────────────_
  _────────────────────────────────────────────────────_
  _───────────────────────────────────────────────────_
  _──────────────────────────────────────────────────_
  _─────────────────────────────────────────────────_
  _────────────────────────────────────────────────_
  _───────────────────────────────────────────────_
  _──────────────────────────────────────────────_
  _─────────────────────────────────────────────_
  _────────────────────────────────────────────_
  _───────────────────────────────────────────_
  _──────────────────────────────────────────_
  _─────────────────────────────────────────_
  _────────────────────────────────────────_
  _───────────────────────────────────────_
  _──────────────────────────────────────_
  _─────────────────────────────────────_
  _────────────────────────────────────_
  _───────────────────────────────────_
  _──────────────────────────────────_
  _─────────────────────────────────_
  _────────────────────────────────_
  _───────────────────────────────_
  _──────────────────────────────_
  _─────────────────────────────_
  _────────────────────────────_
  _───────────────────────────_
  _──────────────────────────_
  _─────────────────────────_
  _────────────────────────_
  _───────────────────────_
  _──────────────────────_
  _─────────────────────_
  _────────────────────_
  _───────────────────_
  _──────────────────_
  _─────────────────_
  _────────────────_
  _───────────────_
  _──────────────_
  _─────────────_
  _────────────_
  _───────────_
  _──────────_
  _─────────_
  _────────_
  _───────_
  _──────_
  _─────_
  _────_
  _───_
_──────────────────────────────────────────────────────────────────────────────────────────────────────────────────_
  _─────────────────────────────────────────────────────────────────────────────────────────────────────────────────_
  _────────────────────────────────────────────────────────────────────────────────────────────────────────────────_
  _───────────────────────────────────────────────────────────────────────────────────────────────────────────────_
  _──────────────────────────────────────────────────────────────────────────────────────────────────────────────_
  _─────────────────────────────────────────────────────────────────────────────────────────────────────────────_
  _────────────────────────────────────────────────────────────────────────────────────────────────────────────_
  _───────────────────────────────────────────────────────────────────────────────────────────────────────────_
  _──────────────────────────────────────────────────────────────────────────────────────────────────────────_
  _─────────────────────────────────────────────────────────────────────────────────────────────────────────_
  _────────────────────────────────────────────────────────────────────────────────────────────────────────_
  _───────────────────────────────────────────────────────────────────────────────────────────────────────_
  _──────────────────────────────────────────────────────────────────────────────────────────────────────_
  _─────────────────────────────────────────────────────────────────────────────────────────────────────_
  _────────────────────────────────────────────────────────────────────────────────────────────────────_
  _───────────────────────────────────────────────────────────────────────────────────────────────────_
  _──────────────────────────────────────────────────────────────────────────────────────────────────_
  _─────────────────────────────────────────────────────────────────────────────────────────────────_
  _────────────────────────────────────────────────────────────────────────────────────────────────_
  _───────────────────────────────────────────────────────────────────────────────────────────────_
  _──────────────────────────────────────────────────────────────────────────────────────────────_
  _─────────────────────────────────────────────────────────────────────────────────────────────_
  _────────────────────────────────────────────────────────────────────────────────────────────_
  _───────────────────────────────────────────────────────────────────────────────────────────_
  _──────────────────────────────────────────────────────────────────────────────────────────_
  _─────────────────────────────────────────────────────────────────────────────────────────_
  _────────────────────────────────────────────────────────────────────────────────────────_
  _───────────────────────────────────────────────────────────────────────────────────────_
  _──────────────────────────────────────────────────────────────────────────────────────_
  _─────────────────────────────────────────────────────────────────────────────────────_
  _────────────────────────────────────────────────────────────────────────────────────_
  _───────────────────────────────────────────────────────────────────────────────────_
  _──────────────────────────────────────────────────────────────────────────────────_
  _─────────────────────────────────────────────────────────────────────────────────_
  _────────────────────────────────────────────────────────────────────────────────_
  _───────────────────────────────────────────────────────────────────────────────_
  _──────────────────────────────────────────────────────────────────────────────_
  _─────────────────────────────────────────────────────────────────────────────_
  _────────────────────────────────────────────────────────────────────────────_
  _───────────────────────────────────────────────────────────────────────────_
  _──────────────────────────────────────────────────────────────────────────_
  _─────────────────────────────────────────────────────────────────────────_
  _────────────────────────────────────────────────────────────────────────_
  _───────────────────────────────────────────────────────────────────────_
  _──────────────────────────────────────────────────────────────────────_
  _─────────────────────────────────────────────────────────────────────_
  _────────────────────────────────────────────────────────────────────_
  _───────────────────────────────────────────────────────────────────_
  _──────────────────────────────────────────────────────────────────_
  _─────────────────────────────────────────────────────────────────_
  _────────────────────────────────────────────────────────────────_
  _───────────────────────────────────────────────────────────────_
  _──────────────────────────────────────────────────────────────_
  _─────────────────────────────────────────────────────────────_
  _────────────────────────────────────────────────────────────_
  _───────────────────────────────────────────────────────────_
  _──────────────────────────────────────────────────────────_
  _─────────────────────────────────────────────────────────_
  _────────────────────────────────────────────────────────_
  _───────────────────────────────────────────────────────_
  _──────────────────────────────────────────────────────_
  _─────────────────────────────────────────────────────_
  _────────────────────────────────────────────────────_
  _───────────────────────────────────────────────────_
  _──────────────────────────────────────────────────_
  _─────────────────────────────────────────────────_
  _────────────────────────────────────────────────_
  _───────────────────────────────────────────────_
  _──────────────────────────────────────────────_
  _─────────────────────────────────────────────_
  _────────────────────────────────────────────_
  _───────────────────────────────────────────_
  _──────────────────────────────────────────_
  _─────────────────────────────────────────_
  _────────────────────────────────────────_
  _───────────────────────────────────────_
  _──────────────────────────────────────_
  _─────────────────────────────────────_
  _────────────────────────────────────_
  _───────────────────────────────────_
  _──────────────────────────────────_
  _─────────────────────────────────_
  _────────────────────────────────_
  _───────────────────────────────_
  _──────────────────────────────_
  _─────────────────────────────_
  _────────────────────────────_
  _───────────────────────────_
  _──────────────────────────_
  _─────────────────────────_
  _────────────────────────_
  _───────────────────────_
  _──────────────────────_
  _─────────────────────_
  _────────────────────_
  _───────────────────_
  _──────────────────_
  _─────────────────_
  _────────────────_
  _───────────────_
  _──────────────_
  _─────────────_
  _────────────_
  _───────────_
  _──────────_
  _─────────_
  _────────_
  _───────_
  _──────_
  _─────_
  _────_
  _───_
  : Type ℓ → Type ℓ′ → Type (ℓ ⊔ₗ ℓ′)
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
  ──────────────────────────────────────────────────────────────────────────────────────────────────────────────────_
  ─────────────────────────────────────────────────────────────────────────────────────────────────────────────────_
  ────────────────────────────────────────────────────────────────────────────────────────────────────────────────_
  ───────────────────────────────────────────────────────────────────────────────────────────────────────────────_
  ──────────────────────────────────────────────────────────────────────────────────────────────────────────────_
  ─────────────────────────────────────────────────────────────────────────────────────────────────────────────_
  ────────────────────────────────────────────────────────────────────────────────────────────────────────────_
  ───────────────────────────────────────────────────────────────────────────────────────────────────────────_
  ──────────────────────────────────────────────────────────────────────────────────────────────────────────_
  ─────────────────────────────────────────────────────────────────────────────────────────────────────────_
  ────────────────────────────────────────────────────────────────────────────────────────────────────────_
  ───────────────────────────────────────────────────────────────────────────────────────────────────────_
  ──────────────────────────────────────────────────────────────────────────────────────────────────────_
  ─────────────────────────────────────────────────────────────────────────────────────────────────────_
  ────────────────────────────────────────────────────────────────────────────────────────────────────_
  ───────────────────────────────────────────────────────────────────────────────────────────────────_
  ──────────────────────────────────────────────────────────────────────────────────────────────────_
  ─────────────────────────────────────────────────────────────────────────────────────────────────_
  ────────────────────────────────────────────────────────────────────────────────────────────────_
  ───────────────────────────────────────────────────────────────────────────────────────────────_
  ──────────────────────────────────────────────────────────────────────────────────────────────_
  ─────────────────────────────────────────────────────────────────────────────────────────────_
  ────────────────────────────────────────────────────────────────────────────────────────────_
  ───────────────────────────────────────────────────────────────────────────────────────────_
  ──────────────────────────────────────────────────────────────────────────────────────────_
  ─────────────────────────────────────────────────────────────────────────────────────────_
  ────────────────────────────────────────────────────────────────────────────────────────_
  ───────────────────────────────────────────────────────────────────────────────────────_
  ──────────────────────────────────────────────────────────────────────────────────────_
  ─────────────────────────────────────────────────────────────────────────────────────_
  ────────────────────────────────────────────────────────────────────────────────────_
  ───────────────────────────────────────────────────────────────────────────────────_
  ──────────────────────────────────────────────────────────────────────────────────_
  ─────────────────────────────────────────────────────────────────────────────────_
  ────────────────────────────────────────────────────────────────────────────────_
  ───────────────────────────────────────────────────────────────────────────────_
  ──────────────────────────────────────────────────────────────────────────────_
  ─────────────────────────────────────────────────────────────────────────────_
  ────────────────────────────────────────────────────────────────────────────_
  ───────────────────────────────────────────────────────────────────────────_
  ──────────────────────────────────────────────────────────────────────────_
  ─────────────────────────────────────────────────────────────────────────_
  ────────────────────────────────────────────────────────────────────────_
  ───────────────────────────────────────────────────────────────────────_
  ──────────────────────────────────────────────────────────────────────_
  ─────────────────────────────────────────────────────────────────────_
  ────────────────────────────────────────────────────────────────────_
  ───────────────────────────────────────────────────────────────────_
  ──────────────────────────────────────────────────────────────────_
  ─────────────────────────────────────────────────────────────────_
  ────────────────────────────────────────────────────────────────_
  ───────────────────────────────────────────────────────────────_
  ──────────────────────────────────────────────────────────────_
  ─────────────────────────────────────────────────────────────_
  ────────────────────────────────────────────────────────────_
  ───────────────────────────────────────────────────────────_
  ──────────────────────────────────────────────────────────_
  ─────────────────────────────────────────────────────────_
  ────────────────────────────────────────────────────────_
  ───────────────────────────────────────────────────────_
  ──────────────────────────────────────────────────────_
  ─────────────────────────────────────────────────────_
  ────────────────────────────────────────────────────_
  ───────────────────────────────────────────────────_
  ──────────────────────────────────────────────────_
  ─────────────────────────────────────────────────_
  ────────────────────────────────────────────────_
  ───────────────────────────────────────────────_
  ──────────────────────────────────────────────_
  ─────────────────────────────────────────────_
  ────────────────────────────────────────────_
  ───────────────────────────────────────────_
  ──────────────────────────────────────────_
  ─────────────────────────────────────────_
  ────────────────────────────────────────_
  ───────────────────────────────────────_
  ──────────────────────────────────────_
  ─────────────────────────────────────_
  ────────────────────────────────────_
  ───────────────────────────────────_
  ──────────────────────────────────_
  ─────────────────────────────────_
  ────────────────────────────────_
  ───────────────────────────────_
  ──────────────────────────────_
  ─────────────────────────────_
  ────────────────────────────_
  ───────────────────────────_
  ──────────────────────────_
  ─────────────────────────_
  ────────────────────────_
  ───────────────────────_
  ──────────────────────_
  ─────────────────────_
  ────────────────────_
  ───────────────────_
  ──────────────────_
  ─────────────────_
  ────────────────_
  ───────────────_
  ──────────────_
  ─────────────_
  ────────────_
  ───────────_
  ──────────_
  ─────────_
  ────────_
  ───────_
  ──────_
  ─────_
  ────_
  ───_
──────────────────────────────────────────────────────────────────────────────────────────────────────────────────_
 ─────────────────────────────────────────────────────────────────────────────────────────────────────────────────_
  ────────────────────────────────────────────────────────────────────────────────────────────────────────────────_
   ───────────────────────────────────────────────────────────────────────────────────────────────────────────────_
    ──────────────────────────────────────────────────────────────────────────────────────────────────────────────_
     ─────────────────────────────────────────────────────────────────────────────────────────────────────────────_
      ────────────────────────────────────────────────────────────────────────────────────────────────────────────_
       ───────────────────────────────────────────────────────────────────────────────────────────────────────────_
        ──────────────────────────────────────────────────────────────────────────────────────────────────────────_
         ─────────────────────────────────────────────────────────────────────────────────────────────────────────_
          ────────────────────────────────────────────────────────────────────────────────────────────────────────_
           ───────────────────────────────────────────────────────────────────────────────────────────────────────_
            ──────────────────────────────────────────────────────────────────────────────────────────────────────_
             ─────────────────────────────────────────────────────────────────────────────────────────────────────_
              ────────────────────────────────────────────────────────────────────────────────────────────────────_
               ───────────────────────────────────────────────────────────────────────────────────────────────────_
                ──────────────────────────────────────────────────────────────────────────────────────────────────_
                 ─────────────────────────────────────────────────────────────────────────────────────────────────_
                  ────────────────────────────────────────────────────────────────────────────────────────────────_
                   ───────────────────────────────────────────────────────────────────────────────────────────────_
                    ──────────────────────────────────────────────────────────────────────────────────────────────_
                     ─────────────────────────────────────────────────────────────────────────────────────────────_
                      ────────────────────────────────────────────────────────────────────────────────────────────_
                       ───────────────────────────────────────────────────────────────────────────────────────────_
                        ──────────────────────────────────────────────────────────────────────────────────────────_
                         ─────────────────────────────────────────────────────────────────────────────────────────_
                          ────────────────────────────────────────────────────────────────────────────────────────_
                           ───────────────────────────────────────────────────────────────────────────────────────_
                            ──────────────────────────────────────────────────────────────────────────────────────_
                             ─────────────────────────────────────────────────────────────────────────────────────_
                              ────────────────────────────────────────────────────────────────────────────────────_
                               ───────────────────────────────────────────────────────────────────────────────────_
                                ──────────────────────────────────────────────────────────────────────────────────_
                                 ─────────────────────────────────────────────────────────────────────────────────_
                                  ────────────────────────────────────────────────────────────────────────────────_
                                   ───────────────────────────────────────────────────────────────────────────────_
                                    ──────────────────────────────────────────────────────────────────────────────_
                                     ─────────────────────────────────────────────────────────────────────────────_
                                      ────────────────────────────────────────────────────────────────────────────_
                                       ───────────────────────────────────────────────────────────────────────────_
                                        ──────────────────────────────────────────────────────────────────────────_
                                         ─────────────────────────────────────────────────────────────────────────_
                                          ────────────────────────────────────────────────────────────────────────_
                                           ───────────────────────────────────────────────────────────────────────_
                                            ──────────────────────────────────────────────────────────────────────_
                                             ─────────────────────────────────────────────────────────────────────_
                                              ────────────────────────────────────────────────────────────────────_
                                               ───────────────────────────────────────────────────────────────────_
                                                ──────────────────────────────────────────────────────────────────_
                                                 ─────────────────────────────────────────────────────────────────_
                                                  ────────────────────────────────────────────────────────────────_
                                                   ───────────────────────────────────────────────────────────────_
                                                    ──────────────────────────────────────────────────────────────_
                                                     ─────────────────────────────────────────────────────────────_
                                                      ────────────────────────────────────────────────────────────_
                                                       ───────────────────────────────────────────────────────────_
                                                        ──────────────────────────────────────────────────────────_
                                                         ─────────────────────────────────────────────────────────_
                                                          ────────────────────────────────────────────────────────_
                                                           ───────────────────────────────────────────────────────_
                                                            ──────────────────────────────────────────────────────_
                                                             ─────────────────────────────────────────────────────_
                                                              ────────────────────────────────────────────────────_
                                                               ───────────────────────────────────────────────────_
                                                                ──────────────────────────────────────────────────_
                                                                 ─────────────────────────────────────────────────_
                                                                  ────────────────────────────────────────────────_
                                                                   ───────────────────────────────────────────────_
                                                                    ──────────────────────────────────────────────_
                                                                     ─────────────────────────────────────────────_
                                                                      ────────────────────────────────────────────_
                                                                       ───────────────────────────────────────────_
                                                                        ──────────────────────────────────────────_
                                                                         ─────────────────────────────────────────_
                                                                          ────────────────────────────────────────_
                                                                           ───────────────────────────────────────_
                                                                            ──────────────────────────────────────_
                                                                             ─────────────────────────────────────_
                                                                              ────────────────────────────────────_
                                                                               ───────────────────────────────────_
                                                                                ──────────────────────────────────_
                                                                                 ─────────────────────────────────_
                                                                                  ────────────────────────────────_
                                                                                   ───────────────────────────────_
                                                                                    ──────────────────────────────_
                                                                                     ─────────────────────────────_
                                                                                      ────────────────────────────_
                                                                                       ───────────────────────────_
                                                                                        ──────────────────────────_
                                                                                         ─────────────────────────_
                                                                                          ────────────────────────_
                                                                                           ───────────────────────_
                                                                                            ──────────────────────_
                                                                                             ─────────────────────_
                                                                                              ────────────────────_
                                                                                               ───────────────────_
                                                                                                ──────────────────_
                                                                                                 ─────────────────_
                                                                                                  ────────────────_
                                                                                                   ───────────────_
                                                                                                    ──────────────_
                                                                                                     ─────────────_
                                                                                                      ────────────_
                                                                                                       ───────────_
                                                                                                        ──────────_
                                                                                                         ─────────_
                                                                                                          ────────_
                                                                                                           ───────_
                                                                                                            ──────_
                                                                                                             ─────_
                                                                                                              ────_
                                                                                                               ───_
  : Type ℓ → Type ℓ
────────────────────────────────────────────────────────────────────────────────────────────────────────────────── 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 _∙_
_∙_ : Type ℓ → Type ℓ′ → Type (ℓ ⊔ₗ ℓ′)
A ∙ B = A → B

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

-- ** equivalences

-- syntax for inference rules (separating hypotheses from conclusion)
infix -50
  _══════════════════════════════════════════════════════════════════════════════════════════════════════════════════_
  _═════════════════════════════════════════════════════════════════════════════════════════════════════════════════_
  _════════════════════════════════════════════════════════════════════════════════════════════════════════════════_
  _═══════════════════════════════════════════════════════════════════════════════════════════════════════════════_
  _══════════════════════════════════════════════════════════════════════════════════════════════════════════════_
  _═════════════════════════════════════════════════════════════════════════════════════════════════════════════_
  _════════════════════════════════════════════════════════════════════════════════════════════════════════════_
  _═══════════════════════════════════════════════════════════════════════════════════════════════════════════_
  _══════════════════════════════════════════════════════════════════════════════════════════════════════════_
  _═════════════════════════════════════════════════════════════════════════════════════════════════════════_
  _════════════════════════════════════════════════════════════════════════════════════════════════════════_
  _═══════════════════════════════════════════════════════════════════════════════════════════════════════_
  _══════════════════════════════════════════════════════════════════════════════════════════════════════_
  _═════════════════════════════════════════════════════════════════════════════════════════════════════_
  _════════════════════════════════════════════════════════════════════════════════════════════════════_
  _═══════════════════════════════════════════════════════════════════════════════════════════════════_
  _══════════════════════════════════════════════════════════════════════════════════════════════════_
  _═════════════════════════════════════════════════════════════════════════════════════════════════_
  _════════════════════════════════════════════════════════════════════════════════════════════════_
  _═══════════════════════════════════════════════════════════════════════════════════════════════_
  _══════════════════════════════════════════════════════════════════════════════════════════════_
  _═════════════════════════════════════════════════════════════════════════════════════════════_
  _════════════════════════════════════════════════════════════════════════════════════════════_
  _═══════════════════════════════════════════════════════════════════════════════════════════_
  _══════════════════════════════════════════════════════════════════════════════════════════_
  _═════════════════════════════════════════════════════════════════════════════════════════_
  _════════════════════════════════════════════════════════════════════════════════════════_
  _═══════════════════════════════════════════════════════════════════════════════════════_
  _══════════════════════════════════════════════════════════════════════════════════════_
  _═════════════════════════════════════════════════════════════════════════════════════_
  _════════════════════════════════════════════════════════════════════════════════════_
  _═══════════════════════════════════════════════════════════════════════════════════_
  _══════════════════════════════════════════════════════════════════════════════════_
  _═════════════════════════════════════════════════════════════════════════════════_
  _════════════════════════════════════════════════════════════════════════════════_
  _═══════════════════════════════════════════════════════════════════════════════_
  _══════════════════════════════════════════════════════════════════════════════_
  _═════════════════════════════════════════════════════════════════════════════_
  _════════════════════════════════════════════════════════════════════════════_
  _═══════════════════════════════════════════════════════════════════════════_
  _══════════════════════════════════════════════════════════════════════════_
  _═════════════════════════════════════════════════════════════════════════_
  _════════════════════════════════════════════════════════════════════════_
  _═══════════════════════════════════════════════════════════════════════_
  _══════════════════════════════════════════════════════════════════════_
  _═════════════════════════════════════════════════════════════════════_
  _════════════════════════════════════════════════════════════════════_
  _═══════════════════════════════════════════════════════════════════_
  _══════════════════════════════════════════════════════════════════_
  _═════════════════════════════════════════════════════════════════_
  _════════════════════════════════════════════════════════════════_
  _═══════════════════════════════════════════════════════════════_
  _══════════════════════════════════════════════════════════════_
  _═════════════════════════════════════════════════════════════_
  _════════════════════════════════════════════════════════════_
  _═══════════════════════════════════════════════════════════_
  _══════════════════════════════════════════════════════════_
  _═════════════════════════════════════════════════════════_
  _════════════════════════════════════════════════════════_
  _═══════════════════════════════════════════════════════_
  _══════════════════════════════════════════════════════_
  _═════════════════════════════════════════════════════_
  _════════════════════════════════════════════════════_
  _═══════════════════════════════════════════════════_
  _══════════════════════════════════════════════════_
  _═════════════════════════════════════════════════_
  _════════════════════════════════════════════════_
  _═══════════════════════════════════════════════_
  _══════════════════════════════════════════════_
  _═════════════════════════════════════════════_
  _════════════════════════════════════════════_
  _═══════════════════════════════════════════_
  _══════════════════════════════════════════_
  _═════════════════════════════════════════_
  _════════════════════════════════════════_
  _═══════════════════════════════════════_
  _══════════════════════════════════════_
  _═════════════════════════════════════_
  _════════════════════════════════════_
  _═══════════════════════════════════_
  _══════════════════════════════════_
  _═════════════════════════════════_
  _════════════════════════════════_
  _═══════════════════════════════_
  _══════════════════════════════_
  _═════════════════════════════_
  _════════════════════════════_
  _═══════════════════════════_
  _══════════════════════════_
  _═════════════════════════_
  _════════════════════════_
  _═══════════════════════_
  _══════════════════════_
  _═════════════════════_
  _════════════════════_
  _═══════════════════_
  _══════════════════_
  _═════════════════_
  _════════════════_
  _═══════════════_
  _══════════════_
  _═════════════_
  _════════════_
  _═══════════_
  _══════════_
  _═════════_
  _════════_
  _═══════_
  _══════_
  _═════_
  _════_
  _═══_
_══════════════════════════════════════════════════════════════════════════════════════════════════════════════════_
  _═════════════════════════════════════════════════════════════════════════════════════════════════════════════════_
  _════════════════════════════════════════════════════════════════════════════════════════════════════════════════_
  _═══════════════════════════════════════════════════════════════════════════════════════════════════════════════_
  _══════════════════════════════════════════════════════════════════════════════════════════════════════════════_
  _═════════════════════════════════════════════════════════════════════════════════════════════════════════════_
  _════════════════════════════════════════════════════════════════════════════════════════════════════════════_
  _═══════════════════════════════════════════════════════════════════════════════════════════════════════════_
  _══════════════════════════════════════════════════════════════════════════════════════════════════════════_
  _═════════════════════════════════════════════════════════════════════════════════════════════════════════_
  _════════════════════════════════════════════════════════════════════════════════════════════════════════_
  _═══════════════════════════════════════════════════════════════════════════════════════════════════════_
  _══════════════════════════════════════════════════════════════════════════════════════════════════════_
  _═════════════════════════════════════════════════════════════════════════════════════════════════════_
  _════════════════════════════════════════════════════════════════════════════════════════════════════_
  _═══════════════════════════════════════════════════════════════════════════════════════════════════_
  _══════════════════════════════════════════════════════════════════════════════════════════════════_
  _═════════════════════════════════════════════════════════════════════════════════════════════════_
  _════════════════════════════════════════════════════════════════════════════════════════════════_
  _═══════════════════════════════════════════════════════════════════════════════════════════════_
  _══════════════════════════════════════════════════════════════════════════════════════════════_
  _═════════════════════════════════════════════════════════════════════════════════════════════_
  _════════════════════════════════════════════════════════════════════════════════════════════_
  _═══════════════════════════════════════════════════════════════════════════════════════════_
  _══════════════════════════════════════════════════════════════════════════════════════════_
  _═════════════════════════════════════════════════════════════════════════════════════════_
  _════════════════════════════════════════════════════════════════════════════════════════_
  _═══════════════════════════════════════════════════════════════════════════════════════_
  _══════════════════════════════════════════════════════════════════════════════════════_
  _═════════════════════════════════════════════════════════════════════════════════════_
  _════════════════════════════════════════════════════════════════════════════════════_
  _═══════════════════════════════════════════════════════════════════════════════════_
  _══════════════════════════════════════════════════════════════════════════════════_
  _═════════════════════════════════════════════════════════════════════════════════_
  _════════════════════════════════════════════════════════════════════════════════_
  _═══════════════════════════════════════════════════════════════════════════════_
  _══════════════════════════════════════════════════════════════════════════════_
  _═════════════════════════════════════════════════════════════════════════════_
  _════════════════════════════════════════════════════════════════════════════_
  _═══════════════════════════════════════════════════════════════════════════_
  _══════════════════════════════════════════════════════════════════════════_
  _═════════════════════════════════════════════════════════════════════════_
  _════════════════════════════════════════════════════════════════════════_
  _═══════════════════════════════════════════════════════════════════════_
  _══════════════════════════════════════════════════════════════════════_
  _═════════════════════════════════════════════════════════════════════_
  _════════════════════════════════════════════════════════════════════_
  _═══════════════════════════════════════════════════════════════════_
  _══════════════════════════════════════════════════════════════════_
  _═════════════════════════════════════════════════════════════════_
  _════════════════════════════════════════════════════════════════_
  _═══════════════════════════════════════════════════════════════_
  _══════════════════════════════════════════════════════════════_
  _═════════════════════════════════════════════════════════════_
  _════════════════════════════════════════════════════════════_
  _═══════════════════════════════════════════════════════════_
  _══════════════════════════════════════════════════════════_
  _═════════════════════════════════════════════════════════_
  _════════════════════════════════════════════════════════_
  _═══════════════════════════════════════════════════════_
  _══════════════════════════════════════════════════════_
  _═════════════════════════════════════════════════════_
  _════════════════════════════════════════════════════_
  _═══════════════════════════════════════════════════_
  _══════════════════════════════════════════════════_
  _═════════════════════════════════════════════════_
  _════════════════════════════════════════════════_
  _═══════════════════════════════════════════════_
  _══════════════════════════════════════════════_
  _═════════════════════════════════════════════_
  _════════════════════════════════════════════_
  _═══════════════════════════════════════════_
  _══════════════════════════════════════════_
  _═════════════════════════════════════════_
  _════════════════════════════════════════_
  _═══════════════════════════════════════_
  _══════════════════════════════════════_
  _═════════════════════════════════════_
  _════════════════════════════════════_
  _═══════════════════════════════════_
  _══════════════════════════════════_
  _═════════════════════════════════_
  _════════════════════════════════_
  _═══════════════════════════════_
  _══════════════════════════════_
  _═════════════════════════════_
  _════════════════════════════_
  _═══════════════════════════_
  _══════════════════════════_
  _═════════════════════════_
  _════════════════════════_
  _═══════════════════════_
  _══════════════════════_
  _═════════════════════_
  _════════════════════_
  _═══════════════════_
  _══════════════════_
  _═════════════════_
  _════════════════_
  _═══════════════_
  _══════════════_
  _═════════════_
  _════════════_
  _═══════════_
  _══════════_
  _═════════_
  _════════_
  _═══════_
  _══════_
  _═════_
  _════_
  _═══_
  : Type ℓ → Type ℓ′ → Type (ℓ ⊔ₗ ℓ′)
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


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

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

  _ : Type
  _ = ∀ {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 : Level → Type where
    ruleX :
      ∙ ℓ ≢ 1ℓ
      ∙ ℓ ≢ 2ℓ
        ───────
        X ℓ
  data Y : Level → Type where
    ruleY :
        ℓ ≢ 1ℓ
      → ℓ ≢ 2ℓ
        --—————
      → Y ℓ

  X⇔Y :
    X ℓ
    ═══
    Y ℓ
  X⇔Y = ↝ , ↜
    where ↝ = λ where (ruleX p q) → ruleY p q
          ↜ = λ where (ruleY p q) → ruleX p q