Library UniMath.Foundations.Init
Initial setup unrelated to Univalent Foundations
Notations
Notation "'∏' x .. y , P" := (∀ x, .. (∀ y, P) ..)
(at level 200, x binder, y binder, right associativity) : type_scope.
Notation "'λ' x .. y , t" := (fun x ⇒ .. (fun y ⇒ t) ..)
(at level 200, x binder, y binder, right associativity).
Notation "A -> B" := (∀ (_ : A), B) : type_scope.
Notation "X <- Y" := (Y → X) (at level 90, only parsing, left associativity) : type_scope.
Notation "x → y" := (x → y)
(at level 99, y at level 200, right associativity): type_scope.
Reserved notations
Reserved Notation "x :: y" (at level 60, right associativity).
Reserved Notation "x ++ y" (at level 60, right associativity).
Reserved Notation "p # x" (right associativity, at level 65).
Reserved Notation "a ╝ b" (at level 70, no associativity).
Reserved Notation "X ≃ Y" (at level 80, no associativity).
Reserved Notation "p #' x" (right associativity, at level 65).
Reserved Notation "f ~ g" (at level 70, no associativity).
Reserved Notation "p @ q" (at level 60, right associativity).
Reserved Notation "'¬¬' X" (at level 35, right associativity).
Reserved Notation "x != y" (at level 70).
Reserved Notation "'¬' X" (at level 35, right associativity).
Reserved Notation "A × B" (at level 75, right associativity).
Reserved Notation "C ⟦ a , b ⟧" (at level 49, right associativity).
Reserved Notation "⟦ a ⟧" (at level 48, left associativity).
Reserved Notation "f ;; g" (at level 50, left associativity, format "f ;; g").
Reserved Notation "g ∘ f" (at level 40, left associativity).
Reserved Notation "f · g" (at level 40, left associativity).
Reserved Notation "a --> b" (at level 55).
Reserved Notation "! p " (at level 50, left associativity).
Reserved Notation "p #' x" (right associativity, at level 65).
Reserved Notation "C '^op'" (at level 3, format "C ^op").
Reserved Notation "q '^-1'" (at level 10).
Reserved Notation "a <-- b" (at level 55).
Reserved Notation "[ C , D ]" .
Reserved Notation "C [ a , b ]" (at level 50, left associativity).
Reserved Notation "X ⟶ Y" (at level 39).
Reserved Notation "X ⟹ Y" (at level 39).
Reserved Notation "F ∙ G" (at level 35).
Reserved Notation "X ⊗ Y" (at level 40, left associativity).
Reserved Notation "f '⊗₁' g" (at level 40, left associativity).
Reserved Notation "α '⊗₂' β" (at level 40, left associativity).
Reserved Notation "F ◾ b" (at level 36, left associativity).
Reserved Notation "F ▭ f" (at level 36, left associativity).
Reserved Notation "A ⇒ B" (at level 95, right associativity).
Reserved Notation "X ⇐ c" (at level 94, left associativity).
Reserved Notation "x ⟲ f" (at level 50, left associativity).
Reserved Notation "q ⟳ x" (at level 50, left associativity).
Reserved Notation "p ◽ b" (at level 36).
Reserved Notation "xe ⟲⟲ p" (at level 50, left associativity).
Reserved Notation "r \\ x" (at level 50, left associativity).
Reserved Notation "x // r" (at level 50, left associativity).
Reserved Notation "X ⨿ Y" (at level 50, left associativity).
Reserved Notation "x ,, y" (at level 60, right associativity).
Reserved Notation "A ⊕ B" (at level 50, left associativity).
Reserved Notation "A ↣ B" (at level 50).
Reserved Notation "B ↠ C" (at level 50).
Tactics
Ltac contradicts a b := solve [ induction (a b) | induction (b a) ].
A few more tactics, thanks go to Jason Gross
Ltac simple_rapply p :=
simple refine p ||
simple refine (p _) ||
simple refine (p _ _) ||
simple refine (p _ _ _) ||
simple refine (p _ _ _ _) ||
simple refine (p _ _ _ _ _) ||
simple refine (p _ _ _ _ _ _) ||
simple refine (p _ _ _ _ _ _ _) ||
simple refine (p _ _ _ _ _ _ _ _) ||
simple refine (p _ _ _ _ _ _ _ _ _) ||
simple refine (p _ _ _ _ _ _ _ _ _ _) ||
simple refine (p _ _ _ _ _ _ _ _ _ _ _) ||
simple refine (p _ _ _ _ _ _ _ _ _ _ _ _) ||
simple refine (p _ _ _ _ _ _ _ _ _ _ _ _ _) ||
simple refine (p _ _ _ _ _ _ _ _ _ _ _ _ _ _) ||
simple refine (p _ _ _ _ _ _ _ _ _ _ _ _ _ _ _).
Tactic Notation "use" uconstr(p) := simple_rapply p.
Tactic Notation "transparent" "assert" "(" ident(name) ":" constr(type) ")" :=
simple refine (let name := (_ : type) in _).
Ltac exact_op x :=
let T := type of x in
let G := match goal with |- ?G ⇒ constr:(G) end in
exact (((λ g:G, g) : T → G) x).
Create HintDb rewrite discriminated.
Hint Variables Opaque : rewrite.
Create HintDb typeclass_instances discriminated.