Martin Escardo.

General terminology and notation.

\begin{code}

{-# OPTIONS --safe --without-K #-}

module Notation.General where

open import MLTT.Pi
open import MLTT.Sigma
open import MLTT.Universes
open import MLTT.Id
open import MLTT.Negation public

\end{code}

The notation `Type ๐“ค` should be avoided in favour of `๐“ค ฬ‡`, but some
module do use it.

\begin{code}

Type  = Set
Typeโ‚ = Setโ‚

fiber : {X : ๐“ค ฬ‡ } {Y : ๐“ฅ ฬ‡ } โ†’ (X โ†’ Y) โ†’ Y โ†’ ๐“ค โŠ” ๐“ฅ ฬ‡
fiber f y = ฮฃ x ๊ž‰ domain f , f x ๏ผ y

to-fiber : {X : ๐“ค ฬ‡ } {Y : ๐“ฅ ฬ‡ } (f : X โ†’ Y) (x : X)
         โ†’ fiber f (f x)
to-fiber f x = x , refl

fiber-point : {X : ๐“ค ฬ‡ } {Y : ๐“ฅ ฬ‡ } {f : X โ†’ Y} {y : Y} โ†’ fiber f y โ†’ X
fiber-point = prโ‚

fiber-identification : {X : ๐“ค ฬ‡ } {Y : ๐“ฅ ฬ‡ } {f : X โ†’ Y} {y : Y} (w : fiber f y)
                     โ†’ f (fiber-point w) ๏ผ y
fiber-identification = prโ‚‚

each-fiber-of : {X : ๐“ค ฬ‡ } {Y : ๐“ฅ ฬ‡ }
              โ†’ (X โ†’ Y)
              โ†’ (๐“ค โŠ” ๐“ฅ ฬ‡ โ†’ ๐“ฆ ฬ‡ )
              โ†’ ๐“ฅ โŠ” ๐“ฆ ฬ‡
each-fiber-of f P = โˆ€ y โ†’ P (fiber f y)

fix : {X : ๐“ค ฬ‡ } โ†’ (f : X โ†’ X) โ†’ ๐“ค ฬ‡
fix f = ฮฃ x ๊ž‰ domain f , x ๏ผ f x

from-fix : {X : ๐“ค ฬ‡ } (f : X โ†’ X) โ†’ fix f โ†’ X
from-fix f = prโ‚

from-fix-is-fixed : {X : ๐“ค ฬ‡ } (f : X โ†’ X) (ฯ† : fix f)
                  โ†’ from-fix f ฯ† ๏ผ f (from-fix f ฯ†)
from-fix-is-fixed f = prโ‚‚

reflexive : {X : ๐“ค ฬ‡ } โ†’ (X โ†’ X โ†’ ๐“ฅ ฬ‡ ) โ†’ ๐“ค โŠ” ๐“ฅ ฬ‡
reflexive R = โˆ€ x โ†’ R x x

symmetric : {X : ๐“ค ฬ‡ } โ†’ (X โ†’ X โ†’ ๐“ฅ ฬ‡ ) โ†’ ๐“ค โŠ” ๐“ฅ ฬ‡
symmetric R = โˆ€ x y โ†’ R x y โ†’ R y x

antisymmetric : {X : ๐“ค ฬ‡ } โ†’ (X โ†’ X โ†’ ๐“ฅ ฬ‡ ) โ†’ ๐“ค โŠ” ๐“ฅ ฬ‡
antisymmetric R = โˆ€ x y โ†’ R x y โ†’ R y x โ†’ x ๏ผ y

transitive : {X : ๐“ค ฬ‡ } โ†’ (X โ†’ X โ†’ ๐“ฅ ฬ‡ ) โ†’ ๐“ค โŠ” ๐“ฅ ฬ‡
transitive R = โˆ€ x y z โ†’ R x y โ†’ R y z โ†’ R x z

idempotent-map : {X : ๐“ฅ ฬ‡ } โ†’ (f : X โ†’ X) โ†’ ๐“ฅ ฬ‡
idempotent-map f = โˆ€ x โ†’ f (f x) ๏ผ f x

involutive : {X : ๐“ฅ ฬ‡ } โ†’ (f : X โ†’ X) โ†’ ๐“ฅ ฬ‡
involutive f = โˆ€ x โ†’ f (f x) ๏ผ x

left-neutral : {X : ๐“ค ฬ‡ } โ†’ X โ†’ (X โ†’ X โ†’ X) โ†’ ๐“ค ฬ‡
left-neutral e _ยท_ = โˆ€ x โ†’ e ยท x ๏ผ x

right-neutral : {X : ๐“ค ฬ‡ } โ†’ X โ†’ (X โ†’ X โ†’ X) โ†’ ๐“ค ฬ‡
right-neutral e _ยท_ = โˆ€ x โ†’ x ยท e ๏ผ x

associative : {X : ๐“ค ฬ‡ } โ†’ (X โ†’ X โ†’ X) โ†’ ๐“ค ฬ‡
associative _ยท_ = โˆ€ x y z โ†’ (x ยท y) ยท z ๏ผ x ยท (y ยท z)

associative' : {X : ๐“ค ฬ‡ } โ†’ (X โ†’ X โ†’ X) โ†’ ๐“ค ฬ‡
associative' _ยท_ = โˆ€ x y z โ†’ x ยท (y ยท z) ๏ผ (x ยท y) ยท z

commutative : {X : ๐“ค ฬ‡ } โ†’ (X โ†’ X โ†’ X) โ†’ ๐“ค ฬ‡
commutative _ยท_ = โˆ€ x y โ†’ (x ยท y) ๏ผ (y ยท x)

left-cancellable : {X : ๐“ค ฬ‡ } {Y : ๐“ฅ ฬ‡ } โ†’ (X โ†’ Y) โ†’ ๐“ค โŠ” ๐“ฅ ฬ‡
left-cancellable f = โˆ€ {x x'} โ†’ f x ๏ผ f x' โ†’ x ๏ผ x'

left-cancellable' : {X : ๐“ค ฬ‡ } {Y : ๐“ฅ ฬ‡ } โ†’ (X โ†’ Y) โ†’ ๐“ค โŠ” ๐“ฅ ฬ‡
left-cancellable' f = โˆ€ x x' โ†’ f x ๏ผ f x' โ†’ x ๏ผ x'

right-cancellable : {X : ๐“ค ฬ‡ } {Y : ๐“ฅ ฬ‡ } โ†’ (X โ†’ Y) โ†’ ๐“คฯ‰
right-cancellable f = {๐“ฆ : Universe} {Z : ๐“ฆ ฬ‡ } (g h : codomain f โ†’ Z)
                    โ†’ g โˆ˜ f โˆผ h โˆ˜ f
                    โ†’ g โˆผ h

_โ†”_ : ๐“ค ฬ‡ โ†’ ๐“ฅ ฬ‡ โ†’ ๐“ค โŠ” ๐“ฅ ฬ‡
A โ†” B = (A โ†’ B) ร— (B โ†’ A)

lr-implication : {X : ๐“ค ฬ‡ } {Y : ๐“ฅ ฬ‡ } โ†’ (X โ†” Y) โ†’ (X โ†’ Y)
lr-implication = prโ‚

rl-implication : {X : ๐“ค ฬ‡ } {Y : ๐“ฅ ฬ‡ } โ†’ (X โ†” Y) โ†’ (Y โ†’ X)
rl-implication = prโ‚‚

โ†”-sym : {X : ๐“ค' ฬ‡ } {Y : ๐“ฅ' ฬ‡ } โ†’ X โ†” Y โ†’ Y โ†” X
โ†”-sym (f , g) = (g , f)

โ†”-trans : {X : ๐“ค' ฬ‡ } {Y : ๐“ฅ' ฬ‡ } {Z : ๐“ฆ' ฬ‡ }
        โ†’ X โ†” Y โ†’ Y โ†” Z โ†’ X โ†” Z
โ†”-trans (f , g) (h , k) = (h โˆ˜ f , g โˆ˜ k)

โ†”-refl : {X : ๐“ค' ฬ‡ } โ†’ X โ†” X
โ†”-refl = (id , id)

\end{code}

This is to avoid naming implicit arguments:

\begin{code}

type-of : {X : ๐“ค ฬ‡ } โ†’ X โ†’ ๐“ค ฬ‡
type-of {๐“ค} {X} x = X

\end{code}

We use the following to indicate the type of a subterm (where "โˆถ"
(typed "\:" in emacs) is not the same as ":"):

\begin{code}

-id : (X : ๐“ค ฬ‡ ) โ†’ X โ†’ X
-id X x = x

syntax -id X x = x โˆถ X

\end{code}

This is used for efficiency as a substitute for lazy "let" (or "where"):

\begin{code}

case_of_ : {A : ๐“ค ฬ‡ } {B : A โ†’ ๐“ฅ ฬ‡ } โ†’ (a : A) โ†’ ((a : A) โ†’ B a) โ†’ B a
case x of f = f x

Case_of_ : {A : ๐“ค ฬ‡ } {B : A โ†’ ๐“ฅ ฬ‡ } โ†’ (a : A) โ†’ ((x : A) โ†’ a ๏ผ x โ†’ B a) โ†’ B a
Case x of f = f x refl

{-# NOINLINE case_of_ #-}

\end{code}

Notation to try to make proofs readable:

\begin{code}

need_which-is-given-by_ : (A : ๐“ค ฬ‡ ) โ†’ A โ†’ A
need A which-is-given-by a = a

have_by_ : (A : ๐“ค ฬ‡ ) โ†’ A โ†’ A
have A by a = a

have_so_ : {A : ๐“ค ฬ‡ } {B : ๐“ฅ ฬ‡ } โ†’ A โ†’ B โ†’ B
have a so b = b

have_so-use_ : {A : ๐“ค ฬ‡ } {B : ๐“ฅ ฬ‡ } โ†’ A โ†’ B โ†’ B
have a so-use b = b

have_and_ : {A : ๐“ค ฬ‡ } {B : ๐“ฅ ฬ‡ } โ†’ A โ†’ B โ†’ B
have a and b = b

apply_to_ : {A : ๐“ค ฬ‡ } {B : ๐“ฅ ฬ‡ } โ†’ (A โ†’ B) โ†’ A โ†’ B
apply f to a = f a

have_so-apply_ : {A : ๐“ค ฬ‡ } {B : ๐“ฅ ฬ‡ } โ†’ A โ†’ (A โ†’ B) โ†’ B
have a so-apply f = f a

assume-then : (A : ๐“ค ฬ‡ ) {B : A โ†’ ๐“ฅ ฬ‡ } โ†’ ((a : A) โ†’ B a) โ†’ (a : A) โ†’ B a
assume-then A f x = f x

syntax assume-then A (ฮป x โ†’ b) = assume x โˆถ A then b

assume-and : (A : ๐“ค ฬ‡ ) {B : A โ†’ ๐“ฅ ฬ‡ } โ†’ ((a : A) โ†’ B a) โ†’ (a : A) โ†’ B a
assume-and A f x = f x

syntax assume-and A (ฮป x โ†’ b) = assume x โˆถ A and b

mapsto : {A : ๐“ค ฬ‡ } {B : A โ†’ ๐“ฅ ฬ‡ } โ†’ ((a : A) โ†’ B a) โ†’ (a : A) โ†’ B a
mapsto f = f

syntax mapsto (ฮป x โ†’ b) = x โ†ฆ b

infixr 10 mapsto

Mapsto : (A : ๐“ค ฬ‡ ) {B : A โ†’ ๐“ฅ ฬ‡ } โ†’ ((a : A) โ†’ B a) โ†’ (a : A) โ†’ B a
Mapsto A f = f

syntax Mapsto A (ฮป x โ†’ b) = x ๊ž‰ A โ†ฆ b

infixr 10 Mapsto

\end{code}

Get rid of this:

\begin{code}

ฮฃ! : {X : ๐“ค ฬ‡ } (A : X โ†’ ๐“ฅ ฬ‡ ) โ†’ ๐“ค โŠ” ๐“ฅ ฬ‡
ฮฃ! {๐“ค} {๐“ฅ} {X} A = (ฮฃ x ๊ž‰ X , A x) ร— ((x x' : X) โ†’ A x โ†’ A x' โ†’ x ๏ผ x')

Sigma! : (X : ๐“ค ฬ‡ ) (A : X โ†’ ๐“ฅ ฬ‡ ) โ†’ ๐“ค โŠ” ๐“ฅ ฬ‡
Sigma! X A = ฮฃ! A

syntax Sigma! A (ฮป x โ†’ b) = ฮฃ! x ๊ž‰ A , b

infixr -1 Sigma!

\end{code}

Note: ฮฃ! is to be avoided, in favour of the contractibility of ฮฃ,
following univalent mathematics.

Fixities:

\begin{code}

infixl -1 -id
infix -1 _โ†”_

\end{code}