diff options
| -rw-r--r-- | src/Data/Type/Properties.agda | 8 |
1 files changed, 7 insertions, 1 deletions
diff --git a/src/Data/Type/Properties.agda b/src/Data/Type/Properties.agda index ecfbc92..28667fa 100644 --- a/src/Data/Type/Properties.agda +++ b/src/Data/Type/Properties.agda @@ -18,7 +18,7 @@ open import Data.List.Relation.Unary.Any using (Any) open import Data.Nat using (ℕ; _<_; _≟_; _+_) open import Data.Nat.Induction using (<-wellFounded) open import Data.Nat.Properties -open import Data.Product using () renaming (_,_ to _,′_) +open import Data.Product using (∃₂) renaming (_,_ to _,′_) open import Data.Sum as ⊎ using (_⊎_; fromInj₁; fromInj₂; [_,_]) open import Data.Type mkFresh open import Induction.WellFounded as Wf using (WfRec) @@ -246,3 +246,9 @@ free-≈ (all {α} {A} {β} {B} A≈B) = begin go (bin ⊗ A B) hyp = bin (hyp A (m≤m+n _ _)) (hyp B (m<n+m _ 0<1+n)) go (all α A) hyp = all (λ _ _ → hyp _ (P.subst (_< _) (sym (size-rename _ A)) (n<1+n _))) + +≈-sym : Symmetric _≈_ +≈-sym (var α) = var α +≈-sym unit = unit +≈-sym (bin A≈C B≈D) = bin (≈-sym A≈C) (≈-sym B≈D) +≈-sym (all A≈B) = all (λ γ∉∀β∙B γ∉∀α∙A → ≈-sym (A≈B γ∉∀α∙A γ∉∀β∙B)) |