Skip to content

Notation.General

Martin Escardo.

General terminology and notation.


{-# 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


The notation `Type 𝓀` should be avoided in favour of `𝓀 Μ‡`, but some
module do use it.


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)


This is to avoid naming implicit arguments:


type-of : {X : 𝓀 Μ‡ } β†’ X β†’ 𝓀 Μ‡
type-of {𝓀} {X} x = X


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


-id : (X : 𝓀 Μ‡ ) β†’ X β†’ X
-id X x = x

syntax -id X x = x ∢ X


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


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_ #-}


Notation to try to make proofs readable:


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


Get rid of this:


Ξ£! : {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!


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.


_β†’βŸ¨_⟩_ : (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

by-instance-resolution : {X : 𝓀 Μ‡ } β†’ {{X}} β†’ X
by-instance-resolution  {{x}} = x


Fixities:


infixl -1 -id
infix -1 _↔_
infixr 0 _β†’βŸ¨_⟩_
infixr 0 _β†βŸ¨_⟩_
infixr 0 _suffices-to-show⟨_⟩_
infix  1 _β–’