Update with new changes to Agda
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
This commit is contained in:
parent
f00dabfc93
commit
2ddac38c3f
|
@ -1,7 +1,7 @@
|
|||
module Isomorphism where
|
||||
|
||||
open import Agda.Primitive using (Level) renaming (_⊔_ to _⊔ℓ_)
|
||||
open import Function.Definitions using (Inverseˡ; Inverseʳ; Injective)
|
||||
open import Function.Definitions using (Injective)
|
||||
open import Lattice
|
||||
open import Equivalence
|
||||
open import Relation.Binary.Core using (_Preserves_⟶_ )
|
||||
|
@ -9,6 +9,16 @@ open import Data.Nat using (ℕ)
|
|||
open import Data.Product using (_,_)
|
||||
open import Relation.Nullary using (¬_)
|
||||
|
||||
IsInverseˡ : ∀ {a b} {A : Set a} {B : Set b}
|
||||
(_≈₁_ : A → A → Set a) (_≈₂_ : B → B → Set b)
|
||||
(f : A → B) (g : B → A) → Set b
|
||||
IsInverseˡ {A = A} {B = B} _≈₁_ _≈₂_ f g = ∀ (x : B) → f (g x) ≈₂ x
|
||||
|
||||
IsInverseʳ : ∀ {a b} {A : Set a} {B : Set b}
|
||||
(_≈₁_ : A → A → Set a) (_≈₂_ : B → B → Set b)
|
||||
(f : A → B) (g : B → A) → Set a
|
||||
IsInverseʳ {A = A} {B = B} _≈₁_ _≈₂_ f g = ∀ (x : A) → g (f x) ≈₁ x
|
||||
|
||||
module TransportFiniteHeight
|
||||
{a b : Level} {A : Set a} {B : Set b}
|
||||
{_≈₁_ : A → A → Set a} {_≈₂_ : B → B → Set b}
|
||||
|
@ -20,7 +30,7 @@ module TransportFiniteHeight
|
|||
(f-preserves-≈₁ : f Preserves _≈₁_ ⟶ _≈₂_) (g-preserves-≈₂ : g Preserves _≈₂_ ⟶ _≈₁_)
|
||||
(f-⊔-distr : ∀ (a₁ a₂ : A) → f (a₁ ⊔₁ a₂) ≈₂ ((f a₁) ⊔₂ (f a₂)))
|
||||
(g-⊔-distr : ∀ (b₁ b₂ : B) → g (b₁ ⊔₂ b₂) ≈₁ ((g b₁) ⊔₁ (g b₂)))
|
||||
(inverseˡ : Inverseˡ _≈₁_ _≈₂_ f g) (inverseʳ : Inverseʳ _≈₁_ _≈₂_ f g) where
|
||||
(inverseˡ : IsInverseˡ _≈₁_ _≈₂_ f g) (inverseʳ : IsInverseʳ _≈₁_ _≈₂_ f g) where
|
||||
|
||||
open IsFiniteHeightLattice fhlA using () renaming (_≺_ to _≺₁_; ≺-cong to ≺₁-cong; ≈-equiv to ≈₁-equiv)
|
||||
open IsLattice lB using () renaming (_≺_ to _≺₂_; ≺-cong to ≺₂-cong; ≈-equiv to ≈₂-equiv)
|
||||
|
|
|
@ -27,6 +27,7 @@ open import Data.List.Properties using (∷-injectiveʳ)
|
|||
open import Data.List.Relation.Unary.All using (All)
|
||||
open import Data.List.Relation.Unary.Any using (Any; here; there)
|
||||
open import Relation.Nullary using (¬_)
|
||||
open import Isomorphism using (IsInverseˡ; IsInverseʳ)
|
||||
|
||||
open import Lattice.Map A B _≈₂_ _⊔₂_ _⊓₂_ ≡-dec-A lB
|
||||
using
|
||||
|
@ -105,8 +106,8 @@ module IterProdIsomorphism where
|
|||
|
||||
-- The left inverse is: from (to x) = x
|
||||
from-to-inverseˡ : ∀ {ks : List A} (uks : Unique ks) →
|
||||
Inverseˡ (_≈ᵐ_ {ks}) (_≈ⁱᵖ_ {length ks})
|
||||
(from {ks}) (to {ks} uks)
|
||||
IsInverseˡ (_≈ᵐ_ {ks}) (_≈ⁱᵖ_ {length ks})
|
||||
(from {ks}) (to {ks} uks)
|
||||
from-to-inverseˡ {[]} _ _ = IsEquivalence.≈-refl (IP.≈-equiv 0)
|
||||
from-to-inverseˡ {k ∷ ks'} (push k≢ks' uks') (v , rest)
|
||||
with ((fm' , ufm') , refl) ← to uks' rest in p rewrite sym p =
|
||||
|
@ -121,8 +122,8 @@ module IterProdIsomorphism where
|
|||
--
|
||||
-- The right inverse is: to (from x) = x
|
||||
from-to-inverseʳ : ∀ {ks : List A} (uks : Unique ks) →
|
||||
Inverseʳ (_≈ᵐ_ {ks}) (_≈ⁱᵖ_ {length ks})
|
||||
(from {ks}) (to {ks} uks)
|
||||
IsInverseʳ (_≈ᵐ_ {ks}) (_≈ⁱᵖ_ {length ks})
|
||||
(from {ks}) (to {ks} uks)
|
||||
from-to-inverseʳ {[]} _ (([] , empty) , kvs≡ks) rewrite kvs≡ks =
|
||||
( (λ k v ())
|
||||
, (λ k v ())
|
||||
|
|
|
@ -168,7 +168,7 @@ module _ (≈₁-dec : IsDecidable _≈₁_) (≈₂-dec : IsDecidable _≈₂_)
|
|||
))
|
||||
... | no a₁̷≈a | no b₁̷≈b | ((n₁ , n₂) , ((c₁ , c₂) , n≤n₁+n₂)) =
|
||||
((suc n₁ , suc n₂) , ( (step₁ (a₁≼a , a₁̷≈a) a≈a' c₁ , step₂ (b₁≼b , b₁̷≈b) b≈b' c₂)
|
||||
, ≤-stepsˡ 1 (subst (n ≤_) (sym (+-suc n₁ n₂)) (+-monoʳ-≤ 1 n≤n₁+n₂))
|
||||
, m≤n⇒m≤o+n 1 (subst (n ≤_) (sym (+-suc n₁ n₂)) (+-monoʳ-≤ 1 n≤n₁+n₂))
|
||||
))
|
||||
|
||||
fixedHeight : IsLattice.FixedHeight isLattice (h₁ + h₂)
|
||||
|
|
Loading…
Reference in New Issue
Block a user