source: src/utilities/proper.ma @ 1635

Last change on this file since 1635 was 1635, checked in by tranquil, 8 years ago
  • lists with binders and monads
  • Joint.ma and other temprarily forked, awaiting feedback from Claudio
  • translation of RTLabs → RTL refactored with new tools
File size: 734 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
21interpretation "is proper" 'is_proper f p = (p f f).
22notation "f ⊨ p" with precedence 50 for @{'is_proper $f $p}.
Note: See TracBrowser for help on using the repository browser.