From 2460fef34f35371c43bdf96c3ebff2e37d37ad7a Mon Sep 17 00:00:00 2001
From: gabrielhdt <gabrielhondet@gmail.com>
Date: Sat, 20 Jun 2020 14:01:39 +0200
Subject: [PATCH] Correction: eqcast must operate on top types

Plus proof irrelevance for other casts
---
 encodings/subtype_poly.lp | 16 +++++++++++-----
 1 file changed, 11 insertions(+), 5 deletions(-)

diff --git a/encodings/subtype_poly.lp b/encodings/subtype_poly.lp
index 3427b28..f4f8cae 100644
--- a/encodings/subtype_poly.lp
+++ b/encodings/subtype_poly.lp
@@ -22,10 +22,12 @@ with μ (μ $T) ↪ μ $T // FIXME: can be proved
 symbol π (T: Set): η (μ T) → Bool
 
 // Casting from/to maximal supertype
-constant symbol maxcast {t: Set}: η t → η (μ t)
-constant symbol downcast {t: Set} (x: η (μ t)): ε (π t x) → η t
+symbol maxcast {t: Set}: η t → η (μ t)
+symbol downcast {t: Set} (x: η (μ t)): ε (π t x) → η t
 definition ↑ {t} ≔ maxcast {t}
 definition ↓ {t} ≔ downcast {t}
+symbol _downcast {t: Set}: η (μ t) → η t
+rule downcast {$t} $x _ ↪ _downcast {$t} $x
 
 rule π ($t ~> $u) ↪ λx: η $t → η (μ $u), ∀ (λy, π $u (x y))
 with π (tuple_t $t $u)
@@ -33,9 +35,9 @@ with π (tuple_t $t $u)
 with π (psub {$t} $a)
    ↪ λx: η (μ $t), (π $t x) ∧ (λy: ε (π $t x), $a (↓ x y))
 with π (arrd $b)
-   ↪ λx: η (arrd (λx, μ ($b x))), ∀ (λy, π (μ ($b y)) (x y))
+   ↪ λx: η (arrd (λx, μ ($b x))), ∀ (λy, π ($b y) (x y))
 
-/// A term ‘x’ that has been cast up still verifies the properties to be of its
+/// A term ‘x’ that has been cast up still validates the properties to be of its
 /// former type.
 symbol cstr_maxcast_idem: ε (∀B (λt, ∀ {t} (λx, π t (maxcast x))))
 // or as a rewrite-rule:
@@ -44,7 +46,11 @@ symbol cstr_maxcast_idem: ε (∀B (λt, ∀ {t} (λx, π t (maxcast x))))
 private constant symbol max_eq: Set → Set → Bool
 set infix 6 "≃" ≔ max_eq
 
-symbol eqcast {fr: Set} {to: Set}: ε (fr ≃ to) → η fr → η to
+// fr and to must be supertypes
+symbol eqcast {fr: Set} {to: Set}: ε (fr ≃ to) → η (μ fr) → η (μ to)
+protected symbol _eqcast {fr: Set} {to: Set}: η (μ fr) → η (μ to)
+rule eqcast {$fr} {$to} _ $e ↪ _eqcast {$fr} {$to} $e
+rule _eqcast {$t} {$t} $e ↪ $e
 
 definition compatible (t u: Set) ≔ μ t ≃ μ u
 set infix 6 "~" ≔ compatible
-- 
GitLab