source: src/utilities/proper.ma @ 1640

Last change on this file since 1640 was 1640, checked in by tranquil, 8 years ago
  • finished fork of semantics.ma
  • unification of Errors under the monad notations brings problems in type checking when res and IO are used together. Needs a lot of annotations, and may break the pre-fork material
File size: 756 bytes
Line 
1include "basics/relations.ma".
2
3definition proper ≝ λA,B.λrelA : relation A.λrelB : relation B.
4λf,g : A → B.
5  ∀a,a' : A.relA a a' → relB (f a) (g a').
6
7definition proper_contra ≝ λA,B.λrelA : relation A.λrelB : relation B.
8λf,g : A → B.
9  ∀a,a' : A.relA a' a → relB (f a) (g a').
10
11
12interpretation "proper" 'proper r s = (proper ? ? r s).
13interpretation "proper contravariant" 'proper_contra r s = (proper_contra ? ? r s).
14
15notation "r ++> s" right associative with precedence 51 for
16  @{'proper $r $s}.
17
18notation "r -+> s" right associative with precedence 51 for
19  @{'proper_contra $r $s}.
20
21(* avoid notation from kikcing in in outputm to avoid things like X ⊨ Prod *)
22notation > "f ⊨ p " with precedence 50 for @{$p $f $f}.
Note: See TracBrowser for help on using the repository browser.