+definition IS_ZERO: Z ⤞ PROP ≝ mk_morphism … is_zero ….
+ normalize /3 by conj,injective_plus_r/
+qed.
+
+unification hint 0 ≔ x:Z ;
+ X ≟ IS_ZERO
+(* ---------------------------------------- *) ⊢
+ is_zero x ≡ mor_carr … X x.
+
+(* We can rewrite under any predicate starting with . *)
+example ex6: ∀x,y:Z. x ≃ y → is_zero (x + y) → is_zero (x + x).
+ #x #y #EQ #H @(.†(#‡EQ)) @H
+qed.
+
+(****** Dependent setoids ********)
+
+(* A setoid is essentially a type equipped with its own notion of equality.
+ In a dependent type theory, one expects to be able to both build types (and
+ setoids) dependent on other types (and setoids). Working with families of
+ setoids that depend over a plain type --- i.e. not another setoid --- pauses
+ no additional problem. For example, we can build a setoid out of vectors of
+ length n assigning to it the type ℕ → setoid. All the machinery for setoids
+ just introduced keeps working. On the other hand, types that depend over a
+ setoid require a much more complex machinery and, in practice, it is not
+ advised to try to work with them in an intentional type theory like the one
+ of Matita.
+
+ To understand the issue, imagine that we have defined a family of
+ types I dependent over integers: I: Z → Type. Because 〈0,1〉 and 〈1,2〉 both
+ represent the same integer +1, the two types I 〈0,1〉 and of I 〈1,2〉 should have
+ exactly the same inhabitants. However, being different types, their inhabitants
+ are disjoint. The solution is to equip the type I with a transport function
+ t: ∀n,m:Z. n ≃ m → I n → I m that maps an element of I n to the corresponding
+ element of I m. Starting from this idea, the picture quickly becomes complex
+ when one start considering all the additional equations that the transport
+ functions should satisfy. For example, if p: n ≃ m, then t … p (t … p^-1 x) = x,
+ i.e. the element in I n corresponding to the element in I m that corresponds to
+ x in I n should be exactly x. Moreover, for any function f: ∀n. I n → T n for
+ some other type T dependent over n the following equation should hold:
+ f … (t … p x) = t … p (f … x) (i.e. transporting and applying f should commute
+ because f should be insensitive too up to ≃ to the actual representation of the
+ integral indexes).
+
+ Luckily enough, in practice types dependent overs setoids occur very rarely.
+ Most examples of dependent types are indexed over discrete objects, like
+ natural, integers and rationals, that admit an unique representation.
+ For continuity reasons, types dependent over real numbers can also be
+ represented as types dependent over a dense subset of the reals, like the
+ rational numbers. *)
+
+(****** Avoiding setoids *******)
+
+(* Quotients are used pervasively in mathematics. In many practical situations,
+ for example when dealing with finite objects like pairs of naturals, an unique
+ representation can be imposed, for example by introducing a normalization
+ procedure to be called after every operation. For example, integer numbers can
+ be normalized to either 〈0,n〉 or 〈n,0〉. Or they can be represented as either 0
+ or a non zero number, with the latter being encoded by a boolean (the sign) and
+ a natural (the predecessor of the absolute value). For example, -3 would be
+ represented by NonZero 〈false,2〉, +3 by NonZero 〈true,2〉 and 0 by Zero.
+ Rational numbers n/m can be put in normal form by dividing both n and m by their
+ greatest common divisor, or by picking n=0, m=1 when n is 0. These normal form
+ is an unique representation.
+
+ Imposing an unique representation is not always possible. For example, picking
+ a canonical representative for a Cauchy sequence is not a computable operation.
+ Nevertheless, when possible, avoiding setoids is preferrable:
+ 1) when the Leibniz equality is used, replacing n with m knowing n=m does not
+ require any proof of properness
+ 2) at the moment automation in Matita is only available for Leibniz equalities.
+ By switching to setoids less proofs are automatically found
+ 3) types dependent over plain types do not need ad-hoc transport functions
+ because the rewriting principle for Leibniz equality plays that role and
+ already satisfies for free all required equations
+ 4) normal forms are usually smaller than other forms. By sticking to normal
+ forms both the memory consumption and the computational cost of operations
+ may be reduced. *)