(* Note that carrier has been defined as a coercion so that when S is a setoid
we can write x:S in place of x: carrier S. *)
-(* We use the notation ≃ for the equality over setoid elements. *)
+(* We use the notation ≃ for the equality on setoid elements. *)
notation "hvbox(n break ≃ m)"
non associative with precedence 45
for @{ 'congruent $n $m }.
@(injective_plus_r … H4)
qed.
-(* The two integers (0,1) and (1,2) are equal up to â\89\9d, written
+(* The two integers (0,1) and (1,2) are equal up to â\89\83, written
〈0,1〉 ≃ 〈1,2〉. Unfolding the notation, that corresponds to
eqrel ? (eq_setoid ?) 〈0,1〉 〈1,2〉 which means that the two
pairs are to be compare according to the equivalence relation
; mor_proper: proper … mor_carr
}.
-(* We introduce a notation for morhism using a long arrow. *)
+(* We introduce a notation for morphism using the symbols of an arrow followed by a dot. *)
notation "hvbox(I break ⤞ O)"
right associative with precedence 20
for @{ 'morphism $I $O }.
(* By declaring mor_carr as a coercion it is possible to write f x for
mor_carr f x in order to apply a morphism f to an argument. *)
-(* Example: oppositive of an integer number. We first implement the function
+(* Example: opposite of an integer number. We first implement the function
over Z and then lift it to a morphism. The proof obligation is to prove
properness. *)
definition opp: Z → Z ≝ λc.〈\snd c,\fst c〉.
(* Example: we state that opp is proper and we will prove it without using
automation and without referring to OPP. When we apply the universal mor_proper
- property of morhisms, Matita looks for the morphism associate to opp x and
+ property of morphisms, Matita looks for the morphism associate to opp x and
finds it thanks to the second unification hint above, completing the proof. *)
example ex2: ∀x,y. x ≃ y → opp x ≃ opp y.
#x #y #EQ @mor_proper @EQ
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). *)
+ 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 *******)
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. *)
\ No newline at end of file
+ may be reduced. *)