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.

Ian Ray, 3rd December 2025.

We add a new syntax where we reason with functions chained in sequence which is
analogous to reasoning by chains of equations or equivalences (see
MLTT/Id.lagda and UF/Equiv.lagda to review these ideas). We will include both
compostional and diagrammatic order.

Notice that reasoning in compositional order with g : B โ†’ C and f : A โ†’ B

 C โ†โŸจ g โŸฉ
 B โ†โŸจ f โŸฉ
 A โ–ข

amounts to a function A โ†’ C (via normal composition), but it appears in the
'bottom up' direction. This may seem strange at first, as one might expect
this feature to only be useful in the forward direction, that is, in
diagrammatic order. In fact, the above actually reflects a common mode of proof
where one proves C by observing it suffices to prove B (and supplying a map
from B to C) and then proving B by observing it suffices to prove A (and
supplying a map from A to B). For this reason we provide notation that allows
us to display proofs of this sort.

\begin{code}

_โ†’โŸจ_โŸฉ_ : (X : ๐“ค ฬ‡ ) {Y : ๐“ฅ ฬ‡ } {Z : ๐“ฆ ฬ‡ } โ†’ (X โ†’ Y) โ†’ (Y โ†’ Z) โ†’ (X โ†’ Z)
_ โ†’โŸจ f โŸฉ g = g โˆ˜ f

_โ†โŸจ_โŸฉ_ : {X : ๐“ค ฬ‡ } {Y : ๐“ฅ ฬ‡ } (Z : ๐“ฆ ฬ‡ ) โ†’ (Y โ†’ Z) โ†’ (X โ†’ Y) โ†’ (X โ†’ Z)
_ โ†โŸจ g โŸฉ f = g โˆ˜ f

_suffices-to-showโŸจ_โŸฉ_ : {X : ๐“ค ฬ‡ } {Y : ๐“ฅ ฬ‡ } (Z : ๐“ฆ ฬ‡ )
                      โ†’ (Y โ†’ Z) โ†’ (X โ†’ Y) โ†’ (X โ†’ Z)
_ suffices-to-showโŸจ g โŸฉ f = g โˆ˜ f

_โ–ข : (X : ๐“ค ฬ‡ ) โ†’ X โ†’ X
X โ–ข = id

infix  1 _โ–ข
infixr 0 _โ†’โŸจ_โŸฉ_
infixr 0 _โ†โŸจ_โŸฉ_
infixr 0 _suffices-to-showโŸจ_โŸฉ_

\end{code}

Fixities:

\begin{code}

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

\end{code}