--- /dev/null
+(* (C) 2014 Luca Bressan *)
+
+include "model.ma".
+
+definition eDe: est → est.
+ #I %
+ [ @(De I)
+ | @De_rect_Type1
+ [ #z @(z = c_unit …)
+ | #i * [ 2: #i' @(i ≃ i') | 3,4: #_ #_ ] @falsum
+ | #F1 #F2 #H1 #H2 * [ 3: #F1' #F2' @(H1 F1' ∧ H2 F2') | 2: #_ | 4: #_ #_ ] @falsum
+ | #F1 #F2 #H1 #H2 * [ 4: #F1' #F2' @(H1 F1' ∧ H2 F2') | 2: #_ | 3: #_ #_ ] @falsum
+ ]
+ | %
+ [ @De_rect_CProp0
+ [ %
+ | @rfl
+ | #F1 #F2 #H1 #H2 % [ @H1 | @H2 ]
+ | #F1 #F2 #H1 #H2 % [ @H1 | @H2 ]
+ ]
+ | @De_rect_CProp0
+ [ * [ #_ % | #i #abs @(De_clash_unit_ev I i abs)
+ | #F1 #F2 #abs @(De_clash_unit_times I F1 F2 abs)
+ | #F1 #F2 #abs @(De_clash_unit_plus I F1 F2 abs) ]
+ | #i * [ @falsum_rect_CProp0 | #i' @sym | 3,4: #F1' #F2' #abs @abs ]
+ | #F1 #F2 #H1 #H2 * [ @falsum_rect_CProp0 | #i' #abs @abs
+ | #F1' #F2' * #K1 #K2 % [ @H1 @K1 | @H2 @K2 ]
+ | #F1' #F2' #abs @abs ]
+ | #F1 #F2 #H1 #H2 * [ @falsum_rect_CProp0 | #i' #abs @abs
+ | #F1' #F2' #abs @abs
+ | #F1' #F2' * #K1 #K2 % [ @H1 @K1 | @H2 @K2 ] ]
+ ]
+ | @De_rect_CProp0
+ [ * [ #F'' #_ #h @h
+ | #i' #F'' #abs @(falsum_rect_CProp0 … (De_clash_unit_ev I i' abs))
+ | #F1' #F2' #F'' #abs @(falsum_rect_CProp0 … (De_clash_unit_times I F1' F2' abs))
+ | #F1' #F2' #F'' #abs @(falsum_rect_CProp0 … (De_clash_unit_plus I F1' F2' abs))
+ ]
+ | #i * [ #F'' @falsum_rect_CProp0
+ | #i' * [ #_ #abs @abs
+ | #i'' @tra
+ | 3,4: #F1'' #F2'' #_ #abs @abs
+ ]
+ | 3,4: #F1' #F2' #F'' @falsum_rect_CProp0
+ ]
+ | #F1 #F2 #H1 #H2 * [ #F'' @falsum_rect_CProp0
+ | #i' #F'' @falsum_rect_CProp0
+ | #F1' #F2' * [ #_ #abs @abs
+ | #i'' #_ #abs @abs
+ | #F1'' #F2'' * #H11 #H12 * #H21 #H22 %
+ [ @(H1 F1' F1'' H11 H21) | @(H2 F2' F2'' H12 H22) ]
+ | #F1'' #F2'' #_ #abs @abs
+ ]
+ | #F1' #F2' #F'' @falsum_rect_CProp0
+ ]
+ | #F1 #F2 #H1 #H2 * [ #F'' @falsum_rect_CProp0
+ | #i' #F'' @falsum_rect_CProp0
+ | #F1' #F2' #F'' @falsum_rect_CProp0
+ | #F1' #F2' * [ #_ #abs @abs
+ | #i'' #_ #abs @abs
+ | #F1'' #F2'' #_ #abs @abs
+ | #F1'' #F2'' * #H11 #H12 * #H21 #H22 %
+ [ @(H1 F1' F1'' H11 H21) | @(H2 F2' F2'' H12 H22) ]
+ ]
+ ]
+ ]
+ ]
+ ]
+qed.
+
--- /dev/null
+(* (C) 2014 Luca Bressan *)
+
+include "model.ma".
+include "pisigma.ma".
+include "pisigma2.ma".
+
+definition en0: est ≝
+ mk_est n0 (λz,z'. z = z') ?.
+ % #x [ % | #y * % | #y #z #h * @h ]
+qed.
+
+definition en0_rect_Type0: ∀Q: edst en0. epi en0 Q ≝
+ λQ. 〈n0_rect_Type0 …, ?〉.
+ @(n0_rect_CProp0).
+qed.
+
+definition en0_rect_Type1: ∀Q: edcl (est_into_ecl en0). ePi … Q ≝
+ λQ. 〈n0_rect_Type1 …, ?〉.
+ @(n0_rect_CProp1).
+qed.
+
+definition edn0: ∀I: est. edst I ≝ λI. constant_edst I en0.
+
--- /dev/null
+(* (C) 2014 Luca Bressan *)
+
+include "model.ma".
+
+include "pisigma2.ma".
+include "power_one.ma".
+include "power.ma".
+
+include "pisigma.ma".
+include "empty.ma".
+include "singleton.ma".
+include "list.ma".
+include "plus.ma".
+include "de.ma".
+
+definition eFalsum: eprop ≝ Falsum.
+definition eId: ∀B: ecl. Sup B → Sup B → eprop ≝ Eq.
+definition eImplies: eprop → eprop → eprop ≝ Implies.
+definition eConj: eprop → eprop → eprop ≝ Conj.
+definition eDisj: eprop → eprop → eprop ≝ Disj.
+
+definition efalsum: eprops ≝ falsum.
+definition eid: ∀B: est. sup B → sup B → eprops ≝ eq.
+definition eimplies: eprops → eprops → eprops ≝ implies.
+definition econj: eprops → eprops → eprops ≝ conj.
+definition edisj: eprops → eprops → eprops ≝ disj.
+
--- /dev/null
+(* (C) 2014 Luca Bressan *)
+
+include "model.ma".
+include "pisigma.ma".
+
+definition proj1: ∀C: est. ∀r: list (Σx. Σy. x ≃ y). list C ≝
+ λC. lift_to_list … (π1 …).
+
+definition proj2: ∀C: est. ∀r: list (Σx. Σy. x ≃ y). list C ≝
+ λC. lift_to_list … (λz: Σx. Σy. x ≃ y. π1 (π2 z)).
+
+definition elist: est → est ≝
+ λC. mk_est
+ (list C)
+ (λz,z'. ∃l: list (Σx. Σy. x ≃ y). (proj1 … l = z) ∧ (proj2 … l = z'))
+ ?.
+ % [ @list_rect_CProp0
+ [ %{ϵ} % %
+ | #l #c * #r * #h1 #h2
+ %{⌈r, 〈c, 〈c, ıc〉〉⌉}
+ % [ @(rewrite_l … ⌈proj1 … r, c⌉
+ (λz. z = ⌈l, c⌉)
+ (rewrite_l … (proj1 … r) (λz. ⌈proj1 … r, c⌉ = ⌈z, c⌉) (reflexivity …) … h1)
+ … (reflexivity …))
+ | @(rewrite_l … ⌈proj2 … r, c⌉
+ (λz. z = ⌈l, c⌉)
+ (rewrite_l … (proj2 … r) (λz. ⌈proj2 … r, c⌉ = ⌈z, c⌉) (reflexivity …) … h2)
+ … (reflexivity …))
+ ]
+ ]
+ | @list_rect_CProp0
+ [ *
+ [ //
+ | #l2' #c * *
+ [ * #_ #abs @(falsum_rect_CProp0 … (list_clash … abs))
+ | #r #s * normalize #abs @(falsum_rect_CProp0 … (list_clash … abs⁻¹))
+ ]
+ ]
+ | #l1' #c1 #h *
+ [ * *
+ [ * #abs @(falsum_rect_CProp0 … (list_clash … abs))
+ | #r #s * #_ normalize #abs @(falsum_rect_CProp0 … (list_clash … abs⁻¹))
+ ]
+ | #l2' #c2 * *
+ [ * #abs @(falsum_rect_CProp0 … (list_clash … abs))
+ | #r #s * #h1 #h2
+ cut (∃l. (proj1 … l = l2') ∧ (proj2 … l = l1'))
+ [ @(h l2') %{r} % [ @(injectivity_cons1 … h1) | @(injectivity_cons1 … h2) ]
+ | * #r' * #h1' #h2' %{⌈r', 〈c2, 〈c1, ?〉〉⌉}
+ [ cut (π1 (π2 s) = c2)
+ [ cut (⌈proj2 … r, π1 (π2 s)⌉ = ⌈l2', c2⌉)
+ [ @(rewrite_l … (proj2 … ⌈r, s⌉)
+ (λz. z = ⌈l2', c2⌉) h2 … (reflexivity …))
+ | @injectivity_cons2
+ ]
+ | #k2 cut (π1 s = c1)
+ [ cut (⌈proj1 … r, sig1 … s⌉ = ⌈l1', c1⌉)
+ [ @(rewrite_l … (proj1 … ⌈r, s⌉)
+ (λz. z = ⌈l1', c1⌉) h1 … (reflexivity …))
+ | @injectivity_cons2
+ ]
+ | #k1 cut (π1 (π2 s) ≃ π1 s)
+ [ @((π2 (π2 s))⁻¹)
+ | #e cut (c2 ≃ π1 s)
+ [ @(rewrite_l … (π1 (π2 s)) (λz. z ≃ π1 s) e … k2)
+ | #e' @(rewrite_l … (π1 s) (λz. c2 ≃ z) e' … k1)
+ ]
+ ]
+ ]
+ ]
+ |
+ % [ @(rewrite_l … (proj1 … r') (λz. ⌈proj1 … r', c2⌉ = ⌈z, c2⌉) (reflexivity …) … h1')
+ | @(rewrite_l … (proj2 … r') (λz. ⌈proj2 … r', c1⌉ = ⌈z, c1⌉) (reflexivity …) … h2')
+ ]
+ ]
+ ]
+ ]
+ ]
+ ]
+ | @list_rect_CProp0
+ [ *
+ [ *
+ [ //
+ | #l3' #c3 #_ //
+ ]
+ | #l2 #c2 *
+ [ #_ #_ %{ϵ} % %
+ | #l3' #c3 * *
+ [ * #_ #abs @(falsum_rect_CProp0 … (list_clash … abs))
+ | #r1' #s1 * #abs @(falsum_rect_CProp0 … (list_clash … abs⁻¹))
+ ]
+ ]
+ ]
+ | #l1' #c1 #h *
+ [ *
+ [ * | #l3' #c3 * ] *
+ [ 1,3: * #abs @(falsum_rect_CProp0 … (list_clash … abs))
+ | 2,4: #r' #s * #_ #abs @(falsum_rect_CProp0 … (list_clash … abs⁻¹))
+ ]
+ | #l2' #c2 *
+ [ #_ * *
+ [ * #abs @(falsum_rect_CProp0 … (list_clash … abs))
+ | #r' #s * #_ #abs @(falsum_rect_CProp0 … (list_clash … abs⁻¹))
+ ]
+ | #l3' #c3 * *
+ [ * #abs @(falsum_rect_CProp0 … (list_clash … abs))
+ | #r1 #s1 * #h1 #h2 * *
+ [ * #abs @(falsum_rect_CProp0 … (list_clash … abs))
+ | #r2 #s2 * #h3 #h4
+ cut (⌈proj1 … r1, π1 s1⌉ = ⌈l1', c1⌉)
+ [ @(rewrite_l … (proj1 … ⌈r1, s1⌉)
+ (λz. z = ⌈l1', c1⌉) h1 … (reflexivity …))
+ | -h1 #h1
+ cut (⌈proj2 … r1, π1 (π2 s1)⌉ = ⌈l2', c2⌉)
+ [ @(rewrite_l … (proj2 … ⌈r1, s1⌉)
+ (λz. z = ⌈l2', c2⌉) h2 … (reflexivity …))
+ | -h2 #h2
+ cut (⌈proj1 … r2, π1 s2⌉ = ⌈l2', c2⌉)
+ [ @(rewrite_l … (proj1 … ⌈r2, s2⌉)
+ (λz. z = ⌈l2', c2⌉) h3 … (reflexivity …))
+ | -h3 #h3
+ cut (⌈proj2 … r2, π1 (π2 s2)⌉ = ⌈l3', c3⌉)
+ [ @(rewrite_l … (proj2 … ⌈r2, s2⌉)
+ (λz. z = ⌈l3', c3⌉) h4 … (reflexivity …))
+ | -h4 #h4
+ cut (∃l. (proj1 … l = l1') ∧ (proj2 … l = l3'))
+ [ @(h l2' l3')
+ [ %{r1} @(mk_conj … (injectivity_cons1 … h1) (injectivity_cons1 … h2))
+ | %{r2} @(mk_conj … (injectivity_cons1 … h3) (injectivity_cons1 … h4))
+ ]
+ | * #r * #e1 #e2 %{⌈r, 〈c1, 〈c3, ?〉〉⌉}
+ [ @(tra …
+ (rewrite_l … (π1 s1) (λz. z ≃ c2)
+ (rewrite_l … (π1 (π2 s1)) (λz. π1 s1 ≃ z) (π2 (π2 s1))
+ … (injectivity_cons2 … h2))
+ … (injectivity_cons2 … h1))
+ (rewrite_l … (π1 (π2 s2)) (λz. c2 ≃ z)
+ (rewrite_l … (π1 s2) (λz. z ≃ π1 (π2 s2)) (π2 (π2 s2))
+ … (injectivity_cons2 … h3))
+ … (injectivity_cons2 … h4)))
+ | %
+ [ @(rewrite_l … (proj1 … r) (λz. ⌈proj1 … r, c1⌉ = ⌈z, c1⌉) (reflexivity …) … e1)
+ | @(rewrite_l … (proj2 … r) (λz. ⌈proj2 … r, c3⌉ = ⌈z, c3⌉) (reflexivity …) … e2)
+ ]
+ ]
+ ]
+ ]
+ ]
+ ]
+ ]
+ ]
+ ]
+ ]
+ ]
+ ]
+ ]
+qed.
+
+definition eepsilon: ∀C: est. elist C ≝ epsilon.
+
+definition econs: ∀C: est. eto (elist C) (eto C (elist C)) ≝
+ λC. 〈λl. 〈cons … l, ?〉, ?〉.
+ [ #c1 #c2 #d
+ cut (subst C (constant_edst C (elist C)) c1 c2 d ⌈l, c1⌉ = ⌈l, c1⌉)
+ [ %
+ | #h @(rewrite_l (list (sup C)) ⌈l, c1⌉ (λz. eq (elist C) z ⌈l, c2⌉) ?
+ (subst C (constant_edst C (elist C)) c1 c2 d ⌈l, c1⌉) h)
+ @(list_rect_CProp0 … l)
+ [ %{⌈ϵ, 〈c1, 〈c2, d〉〉⌉} % %
+ | #l' #c * *
+ [ * #abs @(falsum_rect_CProp0 … (list_clash … abs))
+ | #r' #s * #h1 #h2 %{⌈⌈r', 〈c, 〈c, ıc〉〉⌉, 〈c1, 〈c2, d〉〉⌉} %
+ [ change with (⌈⌈proj1 … , ?⌉, ?⌉) in ⊢ (??%?);
+ cut (proj1 … r' = l')
+ [ @(injectivity_cons1 … h1)
+ | #h @(rewrite_l ????? h) @reflexivity
+ ]
+ | @(rewrite_l … ⌈⌈proj2 … r', c⌉, c2⌉ (λz. z = ⌈⌈l', c⌉, c2⌉) ?
+ (proj2 … ⌈⌈r', 〈c, 〈c, ıc〉〉⌉, 〈c1, 〈c2, d〉〉⌉) (reflexivity …))
+ cut (proj2 … r' = l')
+ [ @(injectivity_cons1 …
+ (rewrite_l … (proj2 … ⌈r', s⌉) (λz. ⌈proj2 … r', sig1 … (sig2 … s)⌉ = z)
+ (reflexivity …) ⌈l', c2⌉ h2))
+ | #h @(rewrite_l … l' (λz. ⌈⌈z, c⌉, c2⌉ = ⌈⌈l', c⌉, c2⌉) (reflexivity …)
+ (proj2 C r') (symmetry … h))
+ ]
+ ]
+ ]
+ ]
+ ]
+ | #l1 #l2 * #r * #h1 #h2 #c %{⌈r, 〈c, 〈c, ıc〉〉⌉} %
+ [ @(rewrite_l … l1 (λz. ⌈z, c⌉ = ⌈l1, c⌉) (reflexivity …) (proj1 … r) (symmetry … h1))
+ | @(rewrite_l … l2 (λz. ⌈z, c⌉ = ⌈l2, c⌉) (reflexivity …) (proj2 … r) (symmetry … h2))
+ ]
+ ]
+qed.
+
--- /dev/null
+(* (C) 2014 Luca Bressan *)
+
+include "notations.ma".
+
+universe constraint Type[0] < Type[1].
+universe constraint Type[1] < Type[2].
+
+notation "'cl'" with precedence 90 for @{ Type[1] }.
+notation "'st'" with precedence 90 for @{ Type[0] }.
+notation "'prop'" with precedence 90 for @{ CProp[1] }.
+notation "'props'" with precedence 90 for @{ CProp[0] }.
+
+record Sigma (B: cl) (C: B → cl) : cl ≝
+ { Sig1: B
+ ; Sig2: C Sig1
+ }.
+interpretation "Strong Indexed Sum" 'sigma x = (Sigma ? x).
+interpretation "Strong Indexed Sum constructor" 'mk_sigma x y = (mk_Sigma ?? x y).
+interpretation "First projection of Strong Indexed Sum" 'sig1 x = (Sig1 ?? x).
+interpretation "Second projection of Strong Indexed Sum" 'sig2 x = (Sig2 ?? x).
+
+definition Times: cl → cl → cl ≝
+ λB,C. Sigma B (λ_. C).
+interpretation "Binary collection product" 'times B C = (Times B C).
+
+inductive n0: st ≝ .
+
+inductive n1: st ≝
+ star: n1.
+interpretation "Element of the singleton" 'star = star.
+
+record sigma (B: st) (C : B → st) : st ≝
+ { sig1: B
+ ; sig2: C sig1
+ }.
+interpretation "Strong Indexed Sum set" 'sigma x = (sigma ? x).
+interpretation "Strong Indexed Sum set constructor" 'mk_sigma x y = (mk_sigma ?? x y).
+interpretation "First projection of Strong Indexed Sum set" 'sig1 x = (sig1 ?? x).
+interpretation "Second projection of Strong Indexed Sum set" 'sig2 x = (sig2 ?? x).
+
+definition times: st → st → st ≝
+ λB,C. sigma B (λ_. C).
+interpretation "Binary set product" 'times B C = (times B C).
+
+inductive list (C: st) : st (*CSC: Type[0]*) ≝
+ epsilon: list C
+ | cons: list C → C → list C.
+interpretation "Empty list" 'epsilon = (epsilon ?).
+interpretation "List constructor" 'cons l c = (cons ? l c).
+
+inductive plus (B: st) (C: st) : st ≝
+ inl: B → plus B C
+ | inr: C → plus B C.
+interpretation "Disjoint Sum set" 'plus B C = (plus B C).
+
+inductive Falsum: prop ≝ .
+interpretation "Falsum" 'falsum = Falsum.
+
+inductive Disj (B: prop) (C: prop) : prop ≝
+ lOr: B → Disj B C
+ | rOr: C → Disj B C.
+interpretation "Disjunction" 'disj B C = (Disj B C).
+
+record Conj (B: prop) (C: prop) : prop ≝
+ { Conj1: B
+ ; Conj2: C
+ }.
+interpretation "Conjunction" 'conj B C = (Conj B C).
+
+definition Implies: prop → prop → prop ≝
+ λB,C: prop. B → C.
+interpretation "Implication" 'implies B C = (Implies B C).
+
+record Exists (B: cl) (C: B → prop) : prop ≝
+ { Ex1: B
+ ; Ex2: C Ex1
+ }.
+interpretation "Existential quantification" 'exists x = (Exists ? x).
+interpretation "Existential quantification constructor" 'mk_exists x y = (mk_Exists ?? x y).
+
+definition Forall: ∀B: cl. (B → prop) → prop ≝ λB,C. ∀b: B. C b.
+
+inductive Id (A: cl) (a: A) : A → prop ≝
+ Reflexivity: Id A a a.
+interpretation "Propositional Equality" 'id a b = (Id ? a b).
+interpretation "Reflexivity in Extensional Collections" 'rfl x = (Reflexivity ? x).
+
+definition Verum: prop ≝ Implies Falsum Falsum.
+interpretation "Verum" 'verum = Verum.
+
+inductive falsum: props ≝ .
+interpretation "Small Falsum" 'falsum = falsum.
+
+inductive disj (B: props) (C: props) : props ≝
+ lor: B → disj B C
+ | ror: C → disj B C.
+interpretation "Small Disjunction" 'disj B C = (disj B C).
+
+record conj (B: props) (C: props) : props ≝
+ { conj1: B
+ ; conj2: C
+ }.
+interpretation "Small Conjunction" 'conj B C = (conj B C).
+
+definition implies: props → props → props ≝
+ λB,C. B → C.
+interpretation "Small Implication" 'implies B C = (implies B C).
+
+record exists (B: st) (C: B → props) : props ≝
+ { exs1: B
+ ; exs2: C exs1
+ }.
+interpretation "Small Existential quantification" 'exists x = (exists ? x).
+interpretation "Small Existential quantification constructor" 'mk_exists x y = (mk_exists ?? x y).
+
+definition forall: ∀B: st. (B → props) → props ≝ λB,C. ∀b: B. C b.
+
+inductive id (A: st) (a: A) : A → props ≝
+ reflexivity: id A a a.
+interpretation "Small Propositional Equality" 'id a b = (id ? a b).
+interpretation "Reflexivity in Extensional Sets" 'rfl x = (reflexivity ? x).
+
+definition verum: props ≝ implies falsum falsum.
+interpretation "Verum" 'verum = verum.
+
+definition fun_to_props: st → cl ≝ λB. B → props.
+
+lemma Symmetry: ∀A: cl. ∀x,x': A. x = x' → x' = x.
+ #A #x #x' * %
+qed.
+interpretation "Symmetry in Intensional Collections" 'sym d = (Symmetry ??? d).
+
+lemma Transitivity: ∀A: cl. ∀x,x',x'': A. x = x' → x' = x'' → x = x''.
+ #A #x #x' #x'' * * %
+qed.
+interpretation "Transitivity in Intensional Collections" 'tra d = (Transitivity ???? d).
+
+lemma rewrite_l: ∀A: st. ∀x: A. ∀P: A → props. P x → ∀y: A. x = y → P y.
+ #A #x #P #h #y * @h
+qed.
+
+notation "hvbox(> h)"
+ non associative with precedence 45
+ for @{ 'rewrite_l $h }.
+interpretation "Rewrite left" 'rewrite_l h = (rewrite_l ????? h).
+
+lemma symmetry: ∀A: st. ∀x,x': A. x = x' → x' = x.
+ #A #x #x' * %
+qed.
+interpretation "Symmetry in Intensional Sets" 'sym d = (symmetry ??? d).
+
+notation "hvbox(< h)"
+ non associative with precedence 45
+ for @{ 'rewrite_r $h }.
+interpretation "Rewrite right" 'rewrite_r h = (rewrite_l ????? (symmetry ??? h)).
+
+lemma transitivity: ∀A: st. ∀x,x',x'': A. x = x' → x' = x'' → x = x''.
+ #A #x #x' #x'' * * %
+qed.
+interpretation "Transitivity in Intensional Sets" 'tra d = (transitivity ???? d).
+
+definition lift_to_list: ∀A,A': st. (A → A') → list A → list A' ≝
+ λA,A',f. list_rect_Type0 … (λ_. list A') ϵ (λl,x,l'. ⌈l', f x⌉).
+
+definition proj_l: ∀B,C: st. B → plus B C → B ≝
+ λB,C,b'. plus_rect_Type0 B C (λ_. B) (λb. b) (λ_. b').
+
+definition proj_r: ∀B,C: st. C → plus B C → C ≝
+ λB,C,c'. plus_rect_Type0 B C (λ_. C) (λ_. c') (λc. c).
+
+lemma injectivity_inl: ∀B,C: st. ∀x,x'. inl B C x = inl B C x' → x = x'.
+ #B #C #x #x'
+ @(rewrite_l … (inl … x) (λz. proj_l … x (inl … x) = proj_l … x z)
+ (ı(proj_l … x (inl … x))) (inl … x'))
+qed.
+
+lemma injectivity_inr: ∀B,C: st. ∀y,y'. inr B C y = inr B C y' → y = y'.
+ #B #C #y #y'
+ @(rewrite_l … (inr … y) (λz. proj_r … y (inr … y) = proj_r … y z)
+ (ı(proj_r … y (inr … y))) (inr … y'))
+qed.
+
+lemma injectivity_cons1: ∀C: st. ∀l,l': list C. ∀c,c': C. ⌈l, c⌉ = ⌈l', c'⌉ → l = l'.
+ #C #l1 #l2 #c1 #c2
+ @(rewrite_l … ⌈l1, c1⌉
+ (list_rect_Type1 … (λ_. props) ⊥ (λl,c,h. l1 = l))
+ (ı…) ⌈l2, c2⌉)
+qed.
+
+lemma injectivity_cons2: ∀C: st. ∀l,l': list C. ∀c,c': C. ⌈l, c⌉ = ⌈l', c'⌉ → c = c'.
+ #C #l1 #l2 #c1 #c2
+ @(rewrite_l … ⌈l1, c1⌉
+ (list_rect_Type1 … (λ_. props) ⊥ (λl,c,h. c1 = c))
+ (ı…) ⌈l2, c2⌉)
+qed.
+
+lemma plus_clash: ∀B,C: st. ∀b: B. ∀c: C. inl … b = inr … c → ⊥.
+ #B #C #b #c #h
+ @(rewrite_l … (inl … b) (plus_rect_Type1 … (λ_. props) (λ_. ⊤) (λ_. ⊥))
+ (λx. x) … h)
+qed.
+
+lemma list_clash: ∀C: st. ∀l: list C. ∀c: C. ϵ = ⌈l, c⌉ → ⊥.
+ #C #l #c #h
+ @(rewrite_l … ϵ (list_rect_Type1 … (λ_. props) ⊤ (λ_,_,_. ⊥))
+ (λx. x) … h)
+qed.
+
+definition nat: st ≝ list n1.
+definition zero: nat ≝ ϵ.
+definition succ: nat → nat ≝ λn. cons … n ⋆.
+definition nat_rect_Type0: ∀Q: nat → st. Q zero → (∀n. Q n → Q (succ n)) → ∀n. Q n.
+ #Q #h0 #hi @list_rect_Type0 [ @h0 | #n @n1_rect_Type0 @(hi n) ]
+qed.
+definition nat_rect_Type1: ∀Q: nat → cl. Q zero → (∀n. Q n → Q (succ n)) → ∀n. Q n.
+ #Q #h0 #hi @list_rect_Type1 [ @h0 | #n @n1_rect_Type1 @(hi n) ]
+qed.
+definition nat_rect_CProp0: ∀Q: nat → props. Q zero → (∀n. Q n → Q (succ n)) → ∀n. Q n.
+ #Q #h0 #hi @list_rect_CProp0 [ @h0 | #n @n1_rect_CProp0 @(hi n) ]
+qed.
+definition nat_rect_CProp1: ∀Q: nat → prop. Q zero → (∀n. Q n → Q (succ n)) → ∀n. Q n.
+ #Q #h0 #hi @list_rect_CProp1 [ @h0 | #n @n1_rect_CProp1 @(hi n) ]
+qed.
+
+inductive De (I: st) : st ≝
+ | c_unit: De I
+ | c_ev: I → De I
+ | c_times: De I → De I → De I
+ | c_plus: De I → De I → De I.
+
+definition int: ∀I: st. De I → (I → st) → st.
+ #I @De_rect_Type1
+ [ #_ @n1
+ | #i #X @(X i)
+ | #L #R #intL #intR #X @((intL X)×(intR X))
+ | #L #R #intL #intR #X @((intL X)+(intR X))
+ ]
+qed.
+
+definition napply: nat → (st → st) → st → st.
+ @nat_rect_Type1
+ [ #F #X @X
+ | #_ #F' #F #X @(F' F X)
+ ]
+qed.
+
+definition mu: ∀I: st. (I → De I) → I → st.
+ #I #F #i @(Σn: nat. napply n (λX: st. int I (F i) (λ_. X)) n0)
+qed.
+
+definition is_c_unit: ∀I: st. ∀F: De I. props.
+ #I * [ @verum | #_ @falsum | 3,4: #_ #_ @falsum ]
+qed.
+
+lemma De_clash_unit_ev: ∀I: st. ∀i: I. c_ev I i = c_unit I → falsum.
+ #I #i #h
+ @(rewrite_l (De I) (c_unit I) (is_c_unit I) (λx. x) (c_ev I i) h⁻¹)
+qed.
+lemma De_clash_unit_times: ∀I: st. ∀F,G: De I. c_times I F G = c_unit I → falsum.
+ #I #F #G #h
+ @(rewrite_l (De I) (c_unit I) (is_c_unit I) (λx. x) (c_times I F G) h⁻¹)
+qed.
+lemma De_clash_unit_plus: ∀I: st. ∀F,G: De I. c_plus I F G = c_unit I → falsum.
+ #I #F #G #h
+ @(rewrite_l (De I) (c_unit I) (is_c_unit I) (λx. x) (c_plus I F G) h⁻¹)
+qed.
+
+inductive mu_ (I: st) (F: I → De I) : I → De I → st ≝
+ fold_unit: ∀i: I. mu_ I F i (c_unit I)
+ | fold_ev: ∀i,i': I. mu_ I F i' (F i') → mu_ I F i (c_ev I i')
+ | fold_times: ∀i: I. ∀G1,G2: De I. mu_ I F i G1 → mu_ I F i G2 → mu_ I F i (c_times I G1 G2)
+ | fold_plusL: ∀i: I. ∀G1,G2: De I. mu_ I F i G1 → mu_ I F i (c_plus I G1 G2)
+ | fold_plusR: ∀i: I. ∀G1,G2: De I. mu_ I F i G2 → mu_ I F i (c_plus I G1 G2).
+
--- /dev/null
+(* (C) 2014 Luca Bressan *)\r
+\r
+include "mTT.ma".\r
+\r
+record is_Equiv (Sup: cl) (Eq: Sup → Sup → prop) : prop ≝\r
+ { Rfl_: ∀x. Eq x x\r
+ ; Sym_: ∀x,x'. Eq x x' → Eq x' x\r
+ ; Tra_: ∀x,x',x''. Eq x x' → Eq x' x'' → Eq x x''\r
+ }.\r
+\r
+record ecl: Type[2] ≝ \r
+ { Sup:> cl\r
+ ; Eq: Sup → Sup → prop\r
+ ; is_ecl: is_Equiv Sup Eq\r
+ }.\r
+interpretation "Equality in Extensional Collections" 'eq a b = (Eq ? a b).\r
+\r
+definition Rfl: ∀B: ecl. ∀x: B. x ≃ x ≝\r
+ λB. Rfl_ … (is_ecl B).\r
+interpretation "Reflexivity in Extensional Collections" 'rfl x = (Rfl ? x).\r
+\r
+definition Sym: ∀B: ecl. ∀x,x': B. x ≃ x' → x' ≃ x ≝\r
+ λB. Sym_ … (is_ecl B).\r
+interpretation "Symmetry in Extensional Collections" 'sym d = (Sym ??? d).\r
+\r
+definition Tra: ∀B: ecl. ∀x,x',x'': B. x ≃ x' → x' ≃ x'' → x ≃ x'' ≝\r
+ λB. Tra_ … (is_ecl B).\r
+interpretation "Transitivity in Extensional Collections" 'tra d d' = (Tra ???? d d').\r
+\r
+record is_Subst (A: ecl)\r
+ (dSup: A → ecl)\r
+ (Subst: ∀x1,x2: A. x1 ≃ x2 → dSup x1 → dSup x2) : prop ≝\r
+ { Pres_eq_: ∀x1,x2: A. ∀d: x1 ≃ x2. ∀y,y': dSup x1.\r
+ y ≃ y' → Subst … d y ≃ Subst … d y'\r
+ ; Not_dep_: ∀x1,x2: A. ∀d,d': x1 ≃ x2. ∀y: dSup x1.\r
+ Subst … d y ≃ Subst … d' y\r
+ ; Pres_id_: ∀x: A. ∀y: dSup x.\r
+ Subst … (ı x) y ≃ y\r
+ ; Clos_comp_: ∀x1,x2,x3: A. ∀y: dSup x1. ∀d: x1 ≃ x2. ∀d': x2 ≃ x3.\r
+ Subst … d' (Subst … d y) ≃ Subst … (d•d') y\r
+ }.\r
+\r
+record edcl (A: ecl) : Type[2] ≝ \r
+ { dSup:1> Sup A → ecl\r
+ ; Subst: ∀x1,x2: Sup A. x1 ≃ x2 → Sup (dSup x1) → Sup (dSup x2)\r
+ ; is_edcl: is_Subst A dSup Subst\r
+ }.\r
+interpretation "Substitution morphisms for Extensional Collections"\r
+ 'subst d y = (Subst ???? d y).\r
+\r
+definition Pres_eq: ∀B: ecl. ∀C: edcl B. ∀x1,x2: B. ∀d: x1 ≃ x2. ∀y,y': C x1.\r
+ y ≃ y' → y∘d ≃ y'∘d ≝\r
+ λB,C. Pres_eq_ … (is_edcl … C).\r
+definition Not_dep: ∀B: ecl. ∀C: edcl B. ∀x1,x2: B. ∀d,d': x1 ≃ x2. ∀y: C x1.\r
+ y∘d ≃ y∘d' ≝\r
+ λB,C. Not_dep_ … (is_edcl … C).\r
+definition Pres_id: ∀B: ecl. ∀C: edcl B. ∀x: B. ∀y: C x.\r
+ y∘(ıx) ≃ y ≝\r
+ λB,C. Pres_id_ … (is_edcl … C).\r
+definition Clos_comp: ∀B: ecl. ∀C: edcl B. ∀x1,x2,x3: B. ∀y: C x1. ∀d: x1 ≃ x2. ∀d': x2 ≃ x3.\r
+ y∘d∘d' ≃ y∘d•d' ≝\r
+ λB,C. Clos_comp_ … (is_edcl … C).\r
+\r
+definition constant_edcl: ∀A: ecl. ecl → edcl A ≝\r
+ λA,Y. mk_edcl … (λ_. Y) (λx1,x2,d,y. y) ?.\r
+ % [ #x1 #x2 #d #y #y' #h @h\r
+ | #x1 #x2 #_ #_ #y @(ıy)\r
+ | #_ #y @(ıy)\r
+ | #x1 #x2 #x3 #y #_ #_ @(ıy)\r
+ ]\r
+qed.\r
+\r
+lemma inverse_Subst: ∀B: ecl. ∀C: edcl B. ∀x1,x2: B. ∀d: x1 ≃ x2. ∀y: C x2.\r
+ y∘d⁻¹∘d ≃ y.\r
+ #B #C #x1 #x2 #d #y\r
+ @(Tra … (y∘d⁻¹∘d) (y∘d⁻¹•d) y)\r
+ [ @Clos_comp\r
+ | @(Tra … (y∘d⁻¹•d) (y∘ıx2) y)\r
+ [ @Not_dep | @Pres_id ]\r
+ ]\r
+qed.\r
+\r
+record is_equiv (sup: st) (eq: sup → sup → props) : props ≝\r
+ { rfl_: ∀x. eq x x\r
+ ; sym_: ∀x,x'. eq x x' → eq x' x\r
+ ; tra_: ∀x,x',x''. eq x x' → eq x' x'' → eq x x''\r
+ }.\r
+\r
+record est: Type[1] ≝ \r
+ { sup:> st\r
+ ; eq: sup → sup → props\r
+ ; is_est: is_equiv sup eq\r
+ }.\r
+interpretation "Equality in Extensional Sets" 'eq a b = (eq ? a b).\r
+\r
+definition rfl: ∀B: est. ∀x: B. x ≃ x ≝\r
+ λB. rfl_ … (is_est B).\r
+interpretation "Reflexivity in Extensional Sets" 'rfl x = (rfl ? x).\r
+\r
+definition sym: ∀B: est. ∀x,x': B. x ≃ x' → x' ≃ x ≝\r
+ λB. sym_ … (is_est B).\r
+interpretation "Symmetry in Extensional Sets" 'sym d = (sym ??? d).\r
+\r
+definition tra: ∀B: est. ∀x,x',x'': B. x ≃ x' → x' ≃ x'' → x ≃ x'' ≝\r
+ λB. tra_ … (is_est B).\r
+interpretation "Transitivity in Extensional Sets" 'tra d d' = (tra ???? d d').\r
+\r
+definition est_into_ecl: est → ecl ≝ \r
+ λB. mk_ecl (sup B) (eq B) ?.\r
+ % [ @rfl | @sym | @tra ]\r
+qed.\r
+\r
+record is_subst (A: est)\r
+ (dsup: A → est)\r
+ (subst: ∀x1,x2: A. x1 ≃ x2 → dsup x1 → dsup x2) : props ≝\r
+ { pres_eq_: ∀x1,x2: A. ∀d: x1 ≃ x2. ∀y,y': dsup x1.\r
+ y ≃ y' → subst … d y ≃ subst … d y'\r
+ ; not_dep_: ∀x1,x2: A. ∀d1,d2: x1 ≃ x2. ∀y: dsup x1.\r
+ subst … d1 y ≃ subst … d2 y\r
+ ; pres_id_: ∀x: sup A. ∀y: dsup x.\r
+ subst … (ıx) y ≃ y\r
+ ; clos_comp_: ∀x1,x2,x3: A. ∀y: dsup x1. ∀d1: x1 ≃ x2. ∀d2: x2 ≃ x3.\r
+ subst … d2 (subst … d1 y) ≃ subst … (d1•d2) y\r
+ }.\r
+\r
+record edst (A: est) : Type[1] ≝ \r
+ { dsup:1> sup A → est\r
+ ; subst: ∀x1,x2: sup A. x1 ≃ x2 → sup (dsup x1) → sup (dsup x2)\r
+ ; is_edst: is_subst A dsup subst\r
+ }.\r
+interpretation "Substitution morphisms for Extensional Sets"\r
+ 'subst p a = (subst ???? p a).\r
+\r
+definition pres_eq: ∀B: est. ∀C: edst B. ∀x1,x2: B. ∀d: x1 ≃ x2. ∀y,y': C x1.\r
+ y ≃ y' → y∘d ≃ y'∘d ≝\r
+ λB,C. pres_eq_ … (is_edst … C).\r
+definition not_dep: ∀B: est. ∀C: edst B. ∀x1,x2: B. ∀d,d': x1 ≃ x2. ∀y: C x1.\r
+ y∘d ≃ y∘d' ≝\r
+ λB,C. not_dep_ … (is_edst … C).\r
+definition pres_id: ∀B: est. ∀C: edst B. ∀x: B. ∀y: C x.\r
+ y∘(ıx) ≃ y ≝\r
+ λB,C. pres_id_ … (is_edst … C).\r
+definition clos_comp: ∀B: est. ∀C: edst B. ∀x1,x2,x3: B. ∀y: C x1. ∀d: x1 ≃ x2. ∀d': x2 ≃ x3.\r
+ y∘d∘d' ≃ y∘(d•d') ≝\r
+ λB,C. clos_comp_ … (is_edst … C).\r
+\r
+definition constant_edst: ∀A: est. est → edst A ≝\r
+ λA,Y. mk_edst … (λ_. Y) (λx1,x2,d,y. y) ?.\r
+ % [ #x1 #x2 #d #y #y' #h @h\r
+ | #x1 #x2 #_ #_ #y @(ıy)\r
+ | #_ #y @(ıy)\r
+ | #x1 #x2 #x3 #y #_ #_ @(ıy)\r
+ ]\r
+qed.\r
+\r
+lemma inverse_subst: ∀B: est. ∀C: edst B. ∀x1,x2: B. ∀d: x1 ≃ x2. ∀y: C x2.\r
+ y∘d⁻¹∘d ≃ y.\r
+ #B #C #x1 #x2 #d #y\r
+ @tra [ @(y∘d⁻¹•d)\r
+ | @clos_comp\r
+ | @tra [ @(y∘ıx2) | @not_dep | @pres_id ]\r
+ ]\r
+qed.\r
+\r
+lemma inverse_subst2: ∀B: est. ∀C: edst B. ∀x1,x2: B. ∀d: x1 ≃ x2. ∀y: C x1.\r
+ y∘d∘d⁻¹ ≃ y.\r
+ #B #C #x1 #x2 #d #y @tra [ @(y∘d•d⁻¹)\r
+ | @clos_comp\r
+ | @tra [ @(y∘(ıx1)) | @not_dep | @pres_id ]\r
+ ]\r
+qed.\r
+\r
+lemma eq_reflexivity: ∀B: est. ∀b1,b2: B. b1 = b2 → b1 ≃ b2.\r
+ #B #b1 #b2 #h @(rewrite_l … b1 (λz. b1 ≃ z) (ıb1) … h)\r
+qed.\r
+\r
+definition eprop: Type[2] ≝ prop.\r
+\r
+definition eprop_into_ecl: eprop → ecl ≝\r
+ λP. mk_ecl P (λ_,_. ⊤) ?.\r
+ % //\r
+qed.\r
+\r
+definition eprops: Type[1] ≝ props.\r
+\r
+definition eprops_into_est: eprops → est ≝\r
+ λP. mk_est P (λ_,_. ⊤) ?.\r
+ % //\r
+qed.\r
+\r
--- /dev/null
+(* (C) 2014 Luca Bressan *)
+
+notation "hvbox(a break \to b)"
+ right associative with precedence 20
+ for @{ \forall $_:$a.$b }.
+
+notation < "hvbox(Σ ident i : ty break . p)"
+ left associative with precedence 20
+for @{'sigma (λ${ident i}: $ty. $p) }.
+notation < "hvbox(Σ ident i break . p)"
+ with precedence 20
+for @{'sigma (λ${ident i}. $p) }.
+
+notation > "Σ list1 ident x sep , opt (: T). term 19 Px"
+ with precedence 20
+ for ${ default
+ @{ ${ fold right @{$Px} rec acc @{'sigma (λ${ident x}: $T. $acc)} } }
+ @{ ${ fold right @{$Px} rec acc @{'sigma (λ${ident x}. $acc)} } }
+ }.
+
+notation "hvbox(π1 s)"
+ non associative with precedence 70
+ for @{ 'sig1 $s) }.
+notation "hvbox(π2 s)"
+ non associative with precedence 70
+ for @{ 'sig2 $s) }.
+
+notation "hvbox(〈 term 19 a, break term 19 b 〉)"
+ with precedence 90 for @{ 'mk_sigma $a $b }.
+
+notation "hvbox(B break × C)"
+ left associative with precedence 55
+ for @{ 'times $B $C }.
+
+notation "⋆"
+ non associative with precedence 90
+ for @{ 'star }.
+
+notation "ϵ"
+ non associative with precedence 90
+ for @{ 'epsilon }.
+notation "⌈ l, c ⌉"
+ non associative with precedence 90
+ for @{ 'cons $l $c }.
+
+notation "hvbox(B break + C)"
+ left associative with precedence 50
+ for @{ 'plus $B $C }.
+
+notation "⊥"
+ non associative with precedence 90
+ for @{ 'falsum }.
+
+notation "hvbox(B break ∨ C)"
+ left associative with precedence 50
+ for @{ 'disj $B $C }.
+
+notation "hvbox(B break ∧ C)"
+ left associative with precedence 60
+ for @{ 'conj $B $C }.
+
+notation < "hvbox(B break → C)"
+ left associative with precedence 60
+ for @{ 'implies $B $C }.
+
+notation < "hvbox(∃ ident i : ty break . p)"
+ left associative with precedence 20
+for @{'exists (λ${ident i}: $ty. $p) }.
+notation < "hvbox(∃ ident i break . p)"
+ with precedence 20
+for @{'exists (λ${ident i}. $p) }.
+
+notation > "∃ list1 ident x sep , opt (: T). term 19 Px"
+ with precedence 20
+ for ${ default
+ @{ ${ fold right @{$Px} rec acc @{'exists (λ${ident x}: $T. $acc)} } }
+ @{ ${ fold right @{$Px} rec acc @{'exists (λ${ident x}. $acc)} } }
+ }.
+notation "hvbox(« term 19 a, break term 19 b »)"
+ with precedence 90 for @{ 'mk_exists $a $b }.
+
+notation "⊤"
+ non associative with precedence 90
+ for @{ 'verum }.
+
+notation "hvbox(a break = b)"
+ non associative with precedence 45
+ for @{ 'id $a $b }.
+
+notation "hvbox(a break ≃ b)"
+ non associative with precedence 45
+ for @{ 'eq $a $b }.
+
+notation "hvbox(ı x)"
+ non associative with precedence 90
+ for @{ 'rfl $x }.
+notation "hvbox(d⁻¹)"
+ non associative with precedence 80
+ for @{ 'sym $d }.
+notation "hvbox(d break • d')"
+ left associative with precedence 60
+ for @{ 'tra $d $d' }.
+
+notation "hvbox(y break ∘ d)"
+ non associative with precedence 50
+ for @{ 'subst $d $y }.
+
+notation "hvbox(f ◽ d)"
+ non associative with precedence 40
+ for @{ 'ap $f $d}.
+notation "hvbox(f ˙ d)"
+ non associative with precedence 60
+ for @{ 'sup_f $f $d}.
+
--- /dev/null
+(* (C) 2014 Luca Bressan *)
+
+include "model.ma".
+
+definition epi: ∀B: est. edst B → est ≝
+ λB,C. mk_est
+ (Σh: ∀y: sup B. sup (dsup … C y). ∀y1,y2: sup B. ∀d: y1 ≃ y2. subst … d (h y1) ≃ h y2)
+ (λz,z'. ∀y: sup B. eq … ((sig1 … z) y) ((sig1 … z') y))
+ ?.
+ % [ #x #y @(ı…)
+ | #x #x' #h #y @((h …)⁻¹)
+ | #x #x' #x'' #h1 #h2 #y @((h1 …)•(h2 …))
+ ]
+qed.
+
+interpretation "Properness of set morphisms" 'ap f d = (sig2 ?? f ?? d).
+interpretation "Support of set morphisms" 'sup_f f d = (sig1 ?? f d).
+
+definition eto: est → est → est ≝
+ λB,C. epi B (constant_edst B C).
+
+definition lift: ∀A,B: est. sup (eto A B) → edst B → edst A ≝
+ λA,B,f,C.
+ mk_edst A (λa: sup A. dsup … C (sig1 … f a))
+ (λx1,x2,d. subst … (sig2 … f … d)) ?.
+ letin B' ≝ (constant_edst A B)
+ % [ #x1 #x2 #d #y #y' #e @(pres_eq … e)
+ | #x1 #x2 #d1 #d2 #y @not_dep
+ | #x #y
+ cut (y∘(ı(f˙x)) ≃ y)
+ [ @pres_id
+ | cut (y∘(f◽(ıx)) ≃ y∘ı(f˙x))
+ [ @not_dep
+ | @tra
+ ]
+ ]
+ | #x1 #x2 #x3 #y #d1 #d2
+ cut (y∘(f◽d1)∘(f◽d2) ≃ y∘(f◽d1)•(f◽d2))
+ [ @clos_comp
+ | cut (y∘(f◽d1)•(f◽d2) ≃ y∘(f◽(d1•d2)))
+ [ @not_dep
+ | #e1 #e2 @(e2•e1)
+ ]
+ ]
+ ]
+qed.
+
+definition shift: ∀B: est. edst B → est → edst B.
+ #B #C #D %
+ [ #b @(eto (C b) D)
+ | #x1 #x2 #d #f %
+ [ #y @(f˙(y∘d⁻¹))
+ | #y1 #y2 #e @(f◽…) @pres_eq @e
+ ]
+ | %
+ [ #x1 #x2 #d #f1 #f2 #h #y @(h (y∘d⁻¹))
+ | #x1 #x2 #d1 #d2 #f #y @(f◽…) @not_dep
+ | #x #f #y @(f◽…) cut (y∘(ıx) ≃ y)
+ [ @pres_id
+ | #h @tra [ @(y∘(ıx)) | @not_dep | @pres_id ]
+ ]
+ | #x1 #x2 #x3 #f #d1 #d2 #y @(f◽…)
+ @tra [ @(y∘(d2⁻¹•d1⁻¹)) | @clos_comp | @not_dep ]
+ ]
+ ]
+qed.
+
+definition esigma: ∀B: est. edst B → est ≝
+ λB,C. mk_est
+ (Σy: B. C y)
+ (λz,z'. ∃d: π1 z ≃ π1 z'. (π2 z)∘d ≃ π2 z')
+ ?.
+ % [ * #b #c %{ıb} @pres_id
+ | * #b #c * #b' #c' * #d #h %{(d⁻¹)}
+ @tra [ @(c∘d•d⁻¹)
+ | @tra [ @(c∘d∘d⁻¹) | @pres_eq @(h⁻¹) | @clos_comp ]
+ | @tra [ @(c∘ıb) | @not_dep | @pres_id ]
+ ]
+ | * #b #c * #b' #c' * #b'' #c'' * #d1 #h1 * #d2 #h2 %{(d1•d2)}
+ @tra [ @(c∘d1∘d2)
+ | @sym @clos_comp
+ | @tra [ @(c'∘d2) | @pres_eq @h1 | @h2 ]
+ ]
+ ]
+qed.
+
+definition etimes: est → est → est ≝
+ λB,C. esigma B (constant_edst B C).
+
+definition mk_esigma: ∀B: est. ∀C: edst B. epi B (shift B C (esigma B C)).
+ #B #C %
+ [ #b %
+ [ #c @〈b, c〉
+ | #c1 #c2 #d %{(ıb)}
+ @tra [ @c1 | @pres_id | @d ]
+ ]
+ | #b1 #b2 #d #y %{d} @inverse_subst
+ ]
+qed.
+
+definition esig1: ∀B: est. ∀C: edst B. sup (eto (esigma B C) B) ≝
+ λB,C. 〈π1 …, ?〉.
+ * #b1 #c1 * #b2 #c2 * #db #dc @db
+qed.
+
+definition esig2: ∀B: est. ∀C: edst B. sup (epi (esigma B C) (lift … (esig1 …) C …)) ≝
+ λB,C. 〈π2 …, ?〉.
+ * #b1 #c1 * #b2 #c2 * #db #dc @dc
+qed.
+
--- /dev/null
+(* (C) 2014 Luca Bressan *)
+
+include "model.ma".
+
+definition ePi: ∀B: ecl. edcl B → ecl ≝
+ λB,C. mk_ecl
+ (Σh: ∀y: Sup B. Sup (dSup … C y). ∀y1,y2: Sup B. ∀d: y1 ≃ y2. Subst … d (h y1) ≃ h y2)
+ (λz,z'. ∀y: Sup B. Eq … ((Sig1 … z) y) ((Sig1 … z') y))
+ ?.
+ % [ #x #y @(ı…)
+ | #x #x' #h #y @((h …)⁻¹)
+ | #x #x' #x'' #h1 #h2 #y @((h1 …)•(h2 …))
+ ]
+qed.
+
+interpretation "Properness of col morphisms" 'ap f d = (Sig2 ?? f ?? d).
+interpretation "Support of col morphisms" 'sup_f f d = (Sig1 ?? f d).
+
+definition eTo: ecl → ecl → ecl ≝
+ λB,C. ePi B (constant_edcl B C).
+
+definition Lift: ∀A,B: ecl. Sup (eTo A B) → edcl B → edcl A ≝
+ λA,B,f,C.
+ mk_edcl A (λa: Sup A. dSup … C (Sig1 … f a))
+ (λx1,x2,d. Subst … (Sig2 … f … d)) ?.
+ letin B' ≝ (constant_edcl A B)
+ % [ #x1 #x2 #d #y #y' #e @(Pres_eq … e)
+ | #x1 #x2 #d1 #d2 #y @Not_dep
+ | #x #y
+ cut (y∘(ı(f˙x)) ≃ y)
+ [ @Pres_id
+ | cut (y∘(f◽(ıx)) ≃ y∘ı(f˙x))
+ [ @Not_dep
+ | @Tra
+ ]
+ ]
+ | #x1 #x2 #x3 #y #d1 #d2
+ cut (y∘(f◽d1)∘(f◽d2) ≃ y∘(f◽d1)•(f◽d2))
+ [ @Clos_comp
+ | cut (Eq (C (f˙x3)) (y∘(f◽d1)•(f◽d2)) (y∘(f◽(d1•d2))))
+ [ @Not_dep
+ | #e1 #e2 @(e2•e1)
+ ]
+ ]
+ ]
+qed.
+
+definition Shift: ∀B: ecl. edcl B → ecl → edcl B.
+ #B #C #D %
+ [ #b @(eTo (C b) D)
+ | #x1 #x2 #d #f %
+ [ #y @(f˙(y∘d⁻¹))
+ | #y1 #y2 #e @(f◽…) @Pres_eq @e
+ ]
+ | %
+ [ #x1 #x2 #d #f1 #f2 #h #y @(h (y∘d⁻¹))
+ | #x1 #x2 #d1 #d2 #f #y @(f◽…) @Not_dep
+ | #x #f #y @(f◽…) cut (y∘(ıx) ≃ y)
+ [ @Pres_id
+ | #h @Tra [ @(y∘(ıx)) | @Not_dep | @Pres_id ]
+ ]
+ | #x1 #x2 #x3 #f #d1 #d2 #y @(f◽…)
+ @Tra [ @(y∘(d2⁻¹•d1⁻¹)) | @Clos_comp | @Not_dep ]
+ ]
+ ]
+qed.
+
+definition eSigma: ∀B: ecl. edcl B → ecl ≝
+ λB,C. mk_ecl
+ (Σy: B. C y)
+ (λz,z'. ∃d: π1 z ≃ π1 z'. (π2 z)∘d ≃ π2 z')
+ ?.
+ % [ * #b #c %{ıb} @Pres_id
+ | * #b #c * #b' #c' * #d #h %{(d⁻¹)}
+ @Tra [ @(c∘d•d⁻¹)
+ | @Tra [ @(c∘d∘d⁻¹) | @Pres_eq @(h⁻¹) | @Clos_comp ]
+ | @Tra [ @(c∘ıb) | @Not_dep | @Pres_id ]
+ ]
+ | * #b #c * #b' #c' * #b'' #c'' * #d1 #h1 * #d2 #h2 %{(d1•d2)}
+ @Tra [ @(c∘d1∘d2)
+ | @Sym @Clos_comp
+ | @Tra [ @(c'∘d2) | @Pres_eq @h1 | @h2 ]
+ ]
+ ]
+qed.
+
+definition eTimes: ecl → ecl → ecl ≝
+ λB,C. eSigma B (constant_edcl B C).
+
+definition mk_eSigma: ∀B: ecl. ∀C: edcl B. ePi B (Shift B C (eSigma B C)).
+ #B #C %
+ [ #b %
+ [ #c @〈b, c〉
+ | #c1 #c2 #d %{(ıb)}
+ @Tra [ @c1 | @Pres_id | @d ]
+ ]
+ | #b1 #b2 #d #y %{d} @inverse_Subst
+ ]
+qed.
+
+definition eSig1: ∀B: ecl. ∀C: edcl B. Sup (eTo (eSigma B C) B) ≝
+ λB,C. 〈π1 …, ?〉.
+ * #b1 #c1 * #b2 #c2 * #db #dc @db
+qed.
+
+definition eSig2: ∀B: ecl. ∀C: edcl B. Sup (ePi (eSigma B C) (Lift … (eSig1 …) C …)) ≝
+ λB,C. 〈π2 …, ?〉.
+ * #b1 #c1 * #b2 #c2 * #db #dc @dc
+qed.
+
--- /dev/null
+(* (C) 2014 Luca Bressan *)
+
+include "model.ma".
+include "pisigma.ma".
+
+definition eplus: est → est → est ≝
+ λB,C. mk_est
+ (B+C)
+ (λz,z'. (∃b: B. ∃b': B. (z = inl … b) ∧ ((z' = inl … b') ∧ (b ≃ b')))
+ ∨ (∃c: C. ∃c': C. (z = inr … c) ∧ ((z' = inr … c') ∧ (c ≃ c'))))
+ ?.
+ % [ * #x [ %1 | %2 ] %{x} %{x} %
+ [ 1,3: @(reflexivity …)
+ | 2: @(mk_conj … (reflexivity …) (ıx))
+ | 4: @(mk_conj … (reflexivity …) (ıx))
+ ]
+ | #z1 #z2 * * #x1 * #x2 * #h1 * #h2 #e [ %1 | %2 ] %{x2} %{x1} %
+ [ 1,3: @h2
+ | 2,4: % [ 1,3: @h1
+ | 2,4: @(e⁻¹)
+ ]
+ ]
+ | #z1 #z2 #z3 * * #x1 * #x12 * #h1 * #h12 #e12 * * #x23 * #x3 * #h23 * #h3 #e23
+ [ %1 %{x1} %{x3} %
+ [ @h1
+ | % [ @h3
+ | @(e12•
+ (rewrite_l … x23 (λz. z ≃ x3) e23 …
+ (injectivity_inl … (h12⁻¹•h23)⁻¹)))
+ ]
+ ]
+ | @(falsum_rect_CProp0 … (plus_clash … (h12⁻¹•h23)))
+ | @(falsum_rect_CProp0 … (plus_clash … ((h12⁻¹•h23)⁻¹)))
+ | %2 %{x1} %{x3} %
+ [ @h1
+ | % [ @h3
+ | @(e12•
+ (rewrite_l … x23 (λz. z ≃ x3) e23 …
+ (injectivity_inr … (h12⁻¹•h23)⁻¹)))
+ ]
+ ]
+ ]
+ ]
+qed.
+
+definition einl: ∀B,C: est. eto B (eplus B C) ≝
+ λB,C. 〈inl …, ?〉.
+ #x #y #h %1 %{x} %{y} % % [ % | @h ]
+qed.
+
+definition einr: ∀B,C: est. eto C (eplus B C) ≝
+ λB,C. 〈inr …, ?〉.
+ #x #y #h %2 %{x} %{y} % % [ % | @h ]
+qed.
+
+lemma injectivity_einl: ∀B,C: est. ∀b,b': B. (einl B C)˙b ≃ (einl B C)˙b' → b ≃ b'.
+ #B #C #b #b' * * #z * #z' * #h1 * #h2 #h3
+ [ @(rewrite_l … z (λw. w ≃ b')
+ (rewrite_l … z' (λw. z ≃ w) h3 … (symmetry … (injectivity_inl … h2))) …
+ (symmetry … (injectivity_inl … h1)))
+ | @(falsum_rect_CProp0 … (plus_clash … h1))
+ ]
+qed.
+
+lemma injectivity_einr: ∀B,C: est. ∀c,c': C. (einr B C)˙c ≃ (einr B C)˙c' → c ≃ c'.
+ #B #C #c #c' * * #z * #z' * #h1 * #h2 #h3
+ [ @(falsum_rect_CProp0 … (plus_clash … (symmetry … h1)))
+ | @(rewrite_l … z (λw. w ≃ c')
+ (rewrite_l … z' (λw. z ≃ w) h3 … (symmetry … (injectivity_inr … h2))) …
+ (symmetry … (injectivity_inr … h1)))
+ ]
+qed.
+
+definition edplus: ∀I: est. edst I → edst I → edst I.
+ #I #B #C %
+ [ @(λi. eplus (B i) (C i))
+ | #i1 #i2 #e * #x [ @(inl … (x∘e)) | @(inr … (x∘e)) ]
+ | % [ #i1 #i2 #e * #x1 * #x2 #h
+ cases h * #z1 * #z2 * #h1 * #h2 #d
+ [ 1: %1 %{(x1∘e)} %{(x2∘e)} % [ % | % [ % | @(pres_eq … (injectivity_einl … h)) ]]
+ | 2,4: @(falsum_rect_CProp0 … (plus_clash … h1))
+ | 3: @(falsum_rect_CProp0 … (plus_clash … h2⁻¹))
+ | 5,7: @(falsum_rect_CProp0 … (plus_clash … h1⁻¹))
+ | 6: @(falsum_rect_CProp0 … (plus_clash … h2))
+ | 8: %2 %{(x1∘e)} %{(x2∘e)} % [ % | % [ % | @(pres_eq … (injectivity_einr … h)) ]]
+ ]
+ | #i1 #i2 #e1 #e2 * #x [ %1 | %2 ] %{(x∘e1)} %{(x∘e2)} %
+ [ 1,3: % | 2,4: % [ 1,3: % | 2,4: @not_dep ]]
+ | #i * #x [ %1 | %2 ] %{(x∘ıi)} %{x} %
+ [ 1,3: % | 2,4: % [ 1,3: % | 2,4: @pres_id ]]
+ | #i1 #i2 #i3 * #x #d1 #d2 [ %1 | %2 ] %{(x∘d1∘d2)} %{(x∘d1•d2)} %
+ [ 1,3: % | 2,4: % [ 1,3: % | 2,4: @clos_comp ]]
+ ]
+ ]
+qed.
+
--- /dev/null
+(* (C) 2014 Luca Bressan *)
+
+include "model.ma".
+
+definition fun_to_power_one: est → ecl ≝
+ λB. mk_ecl
+ (Σh: fun_to_props B. ∀y1,y2: B. eq … y1 y2 → (conj (h y1 → h y2) (h y2 → h y1)))
+ (λz,z'. ∀y: B. conj ((Sig1 … z) y → (Sig1 … z') y)
+ (implies ((Sig1 … z') y) ((Sig1 … z) y)))
+ ?.
+ % [ #x #y % #h @h
+ | #x #x' #h #b % #k cases (h b) [ #_ #r | #r #_ ] @(r k)
+ | #x #x' #x'' #h1 #h2 #b cases (h1 b) #k10 #k01 cases (h2 b) #k21 #k12 %
+ #r [ @(k21 (k10 r)) | @(k01 (k12 r)) ]
+ ]
+qed.
+
--- /dev/null
+(* (C) 2014 Luca Bressan *)
+
+include "model.ma".
+
+definition power_one: ecl ≝
+ mk_ecl props (λz,z'. (z → z') ∧ (z' → z)) ?.
+ % [ #x % #h @h
+ | #x #y * #h1 #h2 % [ @h2 | @h1 ]
+ | #x #y #z #h1 #h2 % cases h1 #hxy #hyx cases h2 #hyz #hzy
+ [ #hx @(hyz (hxy hx))
+ | #hz @(hyx (hzy hz))
+ ]
+ ]
+qed.
+
+definition dpower_one: ∀I: ecl. edcl I.
+ #I %
+ [ #i @power_one
+ | #i1 #i2 #e #p @p
+ | %
+ [ #i1 #i2 #_ #y #y' #h @h
+ | #i1 #i2 #_ #_ @Rfl
+ | #i @Rfl
+ | #i1 #i2 #i3 #y #_ #_ @Rfl
+ ]
+ ]
+qed.
+
--- /dev/null
+baseuri=cic:/matita/minimalist_foundation/
--- /dev/null
+(* (C) 2014 Luca Bressan *)
+
+include "model.ma".
+include "pisigma.ma".
+
+definition en1: est ≝
+ mk_est n1 (λz,z'. z = z') ?.
+ % #x [ % | #y * % | #y #z * * % ]
+qed.
+
+definition estar: en1 ≝ ⋆.
+
+definition en1_rect_Type0: ∀Q: edst en1. eto (Q estar) (epi en1 Q).
+ #Q @(〈?, ?〉)
+ [ #h @(〈n1_rect_Type0 (λw. Q w) h, ?〉)
+ * * #d
+ @(rewrite_l … h (λz. (subst … d z) ≃ z) … (n1_rect_Type0 … h estar) (reflexivity …))
+ @tra [ @(h∘(ı…)) | @not_dep | @pres_id ]
+ | #y1 #y2 #d * @d
+ ]
+qed.
+
+definition edn1: ∀I: est. edst I ≝ λI. constant_edst I en1.
+
projects / helm.git / commitdiff