include "basics/relations.ma".

definition proper ≝ λA,B.λrelA : relation A.λrelB : relation B.
λf,g : A → B.
  ∀a,a' : A.relA a a' → relB (f a) (g a').

definition proper_contra ≝ λA,B.λrelA : relation A.λrelB : relation B.
λf,g : A → B.
  ∀a,a' : A.relA a' a → relB (f a) (g a').


interpretation "proper" 'proper r s = (proper ? ? r s).
interpretation "proper contravariant" 'proper_contra r s = (proper_contra ? ? r s).

notation "r ++> s" right associative with precedence 56 for
  @{'proper $r $s}.

notation "r -+> s" right associative with precedence 56 for
  @{'proper_contra $r $s}.

(* avoid notation from kikcing in in outputm to avoid things like X ⊨ Prod *)
notation > "f ⊨ p " with precedence 55 for @{$p $f $f}.