1 (* (C) 2014 Luca Bressan *)
\r
5 record is_Equiv (Sup: cl) (Eq: Sup → Sup → prop) : prop ≝
\r
7 ; Sym_: ∀x,x'. Eq x x' → Eq x' x
\r
8 ; Tra_: ∀x,x',x''. Eq x x' → Eq x' x'' → Eq x x''
\r
11 record ecl: Type[2] ≝
\r
13 ; Eq: Sup → Sup → prop
\r
14 ; is_ecl: is_Equiv Sup Eq
\r
16 interpretation "Equality in Extensional Collections" 'eq a b = (Eq ? a b).
\r
18 definition Rfl: ∀B: ecl. ∀x: B. x ≃ x ≝
\r
19 λB. Rfl_ … (is_ecl B).
\r
20 interpretation "Reflexivity in Extensional Collections" 'rfl x = (Rfl ? x).
\r
22 definition Sym: ∀B: ecl. ∀x,x': B. x ≃ x' → x' ≃ x ≝
\r
23 λB. Sym_ … (is_ecl B).
\r
24 interpretation "Symmetry in Extensional Collections" 'sym d = (Sym ??? d).
\r
26 definition Tra: ∀B: ecl. ∀x,x',x'': B. x ≃ x' → x' ≃ x'' → x ≃ x'' ≝
\r
27 λB. Tra_ … (is_ecl B).
\r
28 interpretation "Transitivity in Extensional Collections" 'tra d d' = (Tra ???? d d').
\r
30 record is_Subst (A: ecl)
\r
32 (Subst: ∀x1,x2: A. x1 ≃ x2 → dSup x1 → dSup x2) : prop ≝
\r
33 { Pres_eq_: ∀x1,x2: A. ∀d: x1 ≃ x2. ∀y,y': dSup x1.
\r
34 y ≃ y' → Subst … d y ≃ Subst … d y'
\r
35 ; Not_dep_: ∀x1,x2: A. ∀d,d': x1 ≃ x2. ∀y: dSup x1.
\r
36 Subst … d y ≃ Subst … d' y
\r
37 ; Pres_id_: ∀x: A. ∀y: dSup x.
\r
39 ; Clos_comp_: ∀x1,x2,x3: A. ∀y: dSup x1. ∀d: x1 ≃ x2. ∀d': x2 ≃ x3.
\r
40 Subst … d' (Subst … d y) ≃ Subst … (d•d') y
\r
43 record edcl (A: ecl) : Type[2] ≝
\r
44 { dSup:1> Sup A → ecl
\r
45 ; Subst: ∀x1,x2: Sup A. x1 ≃ x2 → Sup (dSup x1) → Sup (dSup x2)
\r
46 ; is_edcl: is_Subst A dSup Subst
\r
48 interpretation "Substitution morphisms for Extensional Collections"
\r
49 'subst d y = (Subst ???? d y).
\r
51 definition Pres_eq: ∀B: ecl. ∀C: edcl B. ∀x1,x2: B. ∀d: x1 ≃ x2. ∀y,y': C x1.
\r
52 y ≃ y' → y∘d ≃ y'∘d ≝
\r
53 λB,C. Pres_eq_ … (is_edcl … C).
\r
54 definition Not_dep: ∀B: ecl. ∀C: edcl B. ∀x1,x2: B. ∀d,d': x1 ≃ x2. ∀y: C x1.
\r
56 λB,C. Not_dep_ … (is_edcl … C).
\r
57 definition Pres_id: ∀B: ecl. ∀C: edcl B. ∀x: B. ∀y: C x.
\r
59 λB,C. Pres_id_ … (is_edcl … C).
\r
60 definition Clos_comp: ∀B: ecl. ∀C: edcl B. ∀x1,x2,x3: B. ∀y: C x1. ∀d: x1 ≃ x2. ∀d': x2 ≃ x3.
\r
62 λB,C. Clos_comp_ … (is_edcl … C).
\r
64 definition constant_edcl: ∀A: ecl. ecl → edcl A ≝
\r
65 λA,Y. mk_edcl … (λ_. Y) (λx1,x2,d,y. y) ?.
\r
66 % [ #x1 #x2 #d #y #y' #h @h
\r
67 | #x1 #x2 #_ #_ #y @(ıy)
\r
69 | #x1 #x2 #x3 #y #_ #_ @(ıy)
\r
73 lemma inverse_Subst: ∀B: ecl. ∀C: edcl B. ∀x1,x2: B. ∀d: x1 ≃ x2. ∀y: C x2.
\r
76 @(Tra … (y∘d⁻¹∘d) (y∘d⁻¹•d) y)
\r
78 | @(Tra … (y∘d⁻¹•d) (y∘ıx2) y)
\r
79 [ @Not_dep | @Pres_id ]
\r
83 record is_equiv (sup: st) (eq: sup → sup → props) : props ≝
\r
85 ; sym_: ∀x,x'. eq x x' → eq x' x
\r
86 ; tra_: ∀x,x',x''. eq x x' → eq x' x'' → eq x x''
\r
89 record est: Type[1] ≝
\r
91 ; eq: sup → sup → props
\r
92 ; is_est: is_equiv sup eq
\r
94 interpretation "Equality in Extensional Sets" 'eq a b = (eq ? a b).
\r
96 definition rfl: ∀B: est. ∀x: B. x ≃ x ≝
\r
97 λB. rfl_ … (is_est B).
\r
98 interpretation "Reflexivity in Extensional Sets" 'rfl x = (rfl ? x).
\r
100 definition sym: ∀B: est. ∀x,x': B. x ≃ x' → x' ≃ x ≝
\r
101 λB. sym_ … (is_est B).
\r
102 interpretation "Symmetry in Extensional Sets" 'sym d = (sym ??? d).
\r
104 definition tra: ∀B: est. ∀x,x',x'': B. x ≃ x' → x' ≃ x'' → x ≃ x'' ≝
\r
105 λB. tra_ … (is_est B).
\r
106 interpretation "Transitivity in Extensional Sets" 'tra d d' = (tra ???? d d').
\r
108 definition est_into_ecl: est → ecl ≝
\r
109 λB. mk_ecl (sup B) (eq B) ?.
\r
110 % [ @rfl | @sym | @tra ]
\r
113 record is_subst (A: est)
\r
115 (subst: ∀x1,x2: A. x1 ≃ x2 → dsup x1 → dsup x2) : props ≝
\r
116 { pres_eq_: ∀x1,x2: A. ∀d: x1 ≃ x2. ∀y,y': dsup x1.
\r
117 y ≃ y' → subst … d y ≃ subst … d y'
\r
118 ; not_dep_: ∀x1,x2: A. ∀d1,d2: x1 ≃ x2. ∀y: dsup x1.
\r
119 subst … d1 y ≃ subst … d2 y
\r
120 ; pres_id_: ∀x: sup A. ∀y: dsup x.
\r
122 ; clos_comp_: ∀x1,x2,x3: A. ∀y: dsup x1. ∀d1: x1 ≃ x2. ∀d2: x2 ≃ x3.
\r
123 subst … d2 (subst … d1 y) ≃ subst … (d1•d2) y
\r
126 record edst (A: est) : Type[1] ≝
\r
127 { dsup:1> sup A → est
\r
128 ; subst: ∀x1,x2: sup A. x1 ≃ x2 → sup (dsup x1) → sup (dsup x2)
\r
129 ; is_edst: is_subst A dsup subst
\r
131 interpretation "Substitution morphisms for Extensional Sets"
\r
132 'subst p a = (subst ???? p a).
\r
134 definition pres_eq: ∀B: est. ∀C: edst B. ∀x1,x2: B. ∀d: x1 ≃ x2. ∀y,y': C x1.
\r
135 y ≃ y' → y∘d ≃ y'∘d ≝
\r
136 λB,C. pres_eq_ … (is_edst … C).
\r
137 definition not_dep: ∀B: est. ∀C: edst B. ∀x1,x2: B. ∀d,d': x1 ≃ x2. ∀y: C x1.
\r
139 λB,C. not_dep_ … (is_edst … C).
\r
140 definition pres_id: ∀B: est. ∀C: edst B. ∀x: B. ∀y: C x.
\r
142 λB,C. pres_id_ … (is_edst … C).
\r
143 definition clos_comp: ∀B: est. ∀C: edst B. ∀x1,x2,x3: B. ∀y: C x1. ∀d: x1 ≃ x2. ∀d': x2 ≃ x3.
\r
144 y∘d∘d' ≃ y∘(d•d') ≝
\r
145 λB,C. clos_comp_ … (is_edst … C).
\r
147 definition constant_edst: ∀A: est. est → edst A ≝
\r
148 λA,Y. mk_edst … (λ_. Y) (λx1,x2,d,y. y) ?.
\r
149 % [ #x1 #x2 #d #y #y' #h @h
\r
150 | #x1 #x2 #_ #_ #y @(ıy)
\r
152 | #x1 #x2 #x3 #y #_ #_ @(ıy)
\r
156 lemma inverse_subst: ∀B: est. ∀C: edst B. ∀x1,x2: B. ∀d: x1 ≃ x2. ∀y: C x2.
\r
158 #B #C #x1 #x2 #d #y
\r
161 | @tra [ @(y∘ıx2) | @not_dep | @pres_id ]
\r
165 lemma inverse_subst2: ∀B: est. ∀C: edst B. ∀x1,x2: B. ∀d: x1 ≃ x2. ∀y: C x1.
\r
167 #B #C #x1 #x2 #d #y @tra [ @(y∘d•d⁻¹)
\r
169 | @tra [ @(y∘(ıx1)) | @not_dep | @pres_id ]
\r
173 lemma eq_reflexivity: ∀B: est. ∀b1,b2: B. b1 = b2 → b1 ≃ b2.
\r
174 #B #b1 #b2 #h @(rewrite_l … b1 (λz. b1 ≃ z) (ıb1) … h)
\r
177 definition eprop: Type[2] ≝ prop.
\r
179 definition eprop_into_ecl: eprop → ecl ≝
\r
180 λP. mk_ecl P (λ_,_. ⊤) ?.
\r
184 definition eprops: Type[1] ≝ props.
\r
186 definition eprops_into_est: eprops → est ≝
\r
187 λP. mk_est P (λ_,_. ⊤) ?.
\r