Require Import Category.Morphisms Category.Dual Category.Sum Category.Pi.
Local Set Warnings Append "-notation-overridden".
Require Export Category.Notations.
Local Set Warnings Append "notation-overridden".
Require Import Basics.Utf8.

Infix "∘" := compose : morphism_scope.
Notation "m ⁻¹" := (morphism_inverse m) : morphism_scope.
Infix "≅" := Isomorphic : category_scope.
Notation "x ↠ y" := (Epimorphism x y).
Notation "x ↪ y" := (Monomorphism x y).

Notation "C 'ᵒᵖ'" := (opposite C) : category_scope.

Notation "∀ x .. y , P" := (∀ x, .. (∀ y, P) ..).
Notation "∀ x .. y , P" := (∀ x, .. (∀ y, P) ..) : type_scope.
Notation "∀ x .. y , P" := (pi (fun x ⇒ .. (pi (fun y ⇒ P)) .. )) : category_scope.