include "preamble.ma".
-(* ACZEL CATEGORIES:
+(* ACZEL CATEGORIES
- We use typoids with a compatible membership relation
- The category is intended to be the domain of the membership relation
- The membership relation is necessary because we need to regard the
| ceq_trans: ∀c1,c,c2. cin ? c1 → ces ? c1 c → ceq ? c c2 → ceq ? c1 c2
| ceq_conf : ∀c1,c,c2. cin ? c1 → ces ? c c1 → ceq ? c c2 → ceq ? c1 c2
.
-(*
-(* external universal quantification *)
-inductive call (C:Class) (P:C \to Prop) : Prop ≝
- | call_intro: (\forall c. cin ? c \to P c) \to call C P.
-inductive call2 (C1,C2:Class) (P:C1 \to C2 \to Prop) : Prop \def
- | call2_intro:
- (\forall c1,c2. cin ? c1 \to cin ? c2 \to P c1 c2) \to call2 C1 C2 P.
-*)
-(* notations **************************************************************)
-(*
-(*CSC: the URI must disappear: there is a bug now *)
-interpretation "external for all" 'xforall \eta.x =
- (cic:/matita/limits/Class/defs/call.ind#xpointer(1/1) _ x).
-
-notation < "hvbox(\xforall ident i opt (: ty) break . p)"
- right associative with precedence 20
-for @{ 'xforall ${default
- @{\lambda ${ident i} : $ty. $p}
- @{\lambda ${ident i} . $p}}}.
-
-notation > "\forall list1 ident x sep , opt (: T). term 19 Px"
- with precedence 20
- for ${ default
- @{ ${ fold right @{$Px} rec acc @{'xforall (λ${ident x}:$T.$acc)} } }
- @{ ${ fold right @{$Px} rec acc @{'xforall (λ${ident x}.$acc)} } }
- }.
-
-(*CSC: the URI must disappear: there is a bug now *)
-interpretation "external for all 2" 'xforall2 \eta.x \eta.y =
- (cic:/matita/limits/Class/defs/call2.ind#xpointer(1/1) _ _ x y).
-
-notation > "hvbox(\xforall ident i1 opt (: ty1) ident i2 opt (: ty2) break . p)"
- with precedence 20
-for @{ 'xforall2 ${default
- @{\lambda ${ident i1} : $ty1. \lambda ${ident i2} : $ty2. $p}
- @{\lambda ${ident i1}, ${ident i2}. $p}}}.
-*)