notation ". r" with precedence 50 for @{'fi $r}.
interpretation "fi" 'fi r = (fi' ?? r).
-ndefinition and_morphism: binary_morphism1 CPROP CPROP CPROP.
- napply mk_binary_morphism1
- [ napply And
- | #a; #a'; #b; #b'; *; #H1; #H2; *; #H3; #H4; napply mk_iff; *; #K1; #K2; napply conj
- [ napply (H1 K1)
- | napply (H3 K2)
- | napply (H2 K1)
- | napply (H4 K2)]##]
+ndefinition and_morphism: unary_morphism1 CPROP (unary_morphism1_setoid1 CPROP CPROP).
+ napply (mk_binary_morphism1 … And);
+ #a; #a'; #b; #b'; #Ha; #Hb; @; *; #x; #y; @
+ [ napply (. Ha^-1) | napply (. Hb^-1) | napply (. Ha) | napply (. Hb)] //.
nqed.
-unification hint 0 ≔ A,B ⊢ fun21 … and_morphism A B ≡ And A B.
+unification hint 0 ≔ A,B ⊢
+ mk_unary_morphism1 …
+ (λX.mk_unary_morphism1 … (And X) (prop11 … (and_morphism X)))
+ (prop11 … and_morphism)
+ A B ≡ And A B.
-(*nlemma test: ∀A,A',B: CProp[0]. A=A' → (B ∨ A) = B → (B ∧ A) ∧ B.
- #A; #A'; #B; #H1; #H2;
- napply (. ((#‡H1)‡H2^-1)); nnormalize;
-nqed.*)
+(*
+naxiom daemon: False.
-(*interpretation "and_morphism" 'and a b = (fun21 ??? and_morphism a b).*)
+nlemma test: ∀A,A',B: CProp[0]. A=A' → (B ∨ A) = B → (B ∧ A) ∧ B.
+ #A; #A'; #B; #H1; #H2; napply (. (#‡H1)‡H2^-1); nelim daemon.
+nqed.
+
+CSC: ugly proof term
+ncheck test.
+*)
-ndefinition or_morphism: binary_morphism1 CPROP CPROP CPROP.
- napply mk_binary_morphism1
- [ napply Or
- | #a; #a'; #b; #b'; *; #H1; #H2; *; #H3; #H4; napply mk_iff; *; #H;
- ##[##1,3: napply or_introl |##*: napply or_intror ]
- ##[ napply (H1 H)
- | napply (H2 H)
- | napply (H3 H)
- | napply (H4 H)]##]
+ndefinition or_morphism: unary_morphism1 CPROP (unary_morphism1_setoid1 CPROP CPROP).
+ napply (mk_binary_morphism1 … Or);
+ #a; #a'; #b; #b'; #Ha; #Hb; @; *; #x
+ [ @1; napply (. Ha^-1) | @2; napply (. Hb^-1) | @1; napply (. Ha) | @2; napply (. Hb)] //.
nqed.
-unification hint 0 ≔ A,B ⊢ fun21 … or_morphism A B ≡ Or A B.
+unification hint 0 ≔ A,B ⊢
+ mk_unary_morphism1 …
+ (λX.mk_unary_morphism1 … (Or X) (prop11 … (or_morphism X)))
+ (prop11 … or_morphism)
+ A B ≡ Or A B.
-(*interpretation "or_morphism" 'or a b = (fun21 ??? or_morphism a b).*)
+ndefinition if_morphism: unary_morphism1 CPROP (unary_morphism1_setoid1 CPROP CPROP).
+ napply (mk_binary_morphism1 … (λA,B:CProp[0]. A → B));
+ #a; #a'; #b; #b'; #Ha; #Hb; @; #H; #x
+ [ napply (. Hb^-1); napply H; napply (. Ha) | napply (. Hb); napply H; napply (. Ha^-1)]
+ //.
+nqed.
-ndefinition if_morphism: binary_morphism1 CPROP CPROP CPROP.
- napply mk_binary_morphism1
- [ napply (λA,B. A → B)
- | #a; #a'; #b; #b'; #H1; #H2; napply mk_iff; #H; #w
- [ napply (if … H2); napply H; napply (fi … H1); nassumption
- | napply (fi … H2); napply H; napply (if … H1); nassumption]##]
-nqed.
\ No newline at end of file
+unification hint 0 ≔ A,B ⊢
+ mk_unary_morphism1 …
+ (λX:CProp[0].mk_unary_morphism1 … (λY:CProp[0]. X → Y) (prop11 … (if_morphism X)))
+ (prop11 … if_morphism)
+ A B ≡ A → B.
\ No newline at end of file