ネストされたレコードを使用するより便利な方法はありますか？

Question

私がbeforeに言ったように、私は代数、行列、およびカテゴリ理論についての図書館で働いています。私は代数構造を表すレコード型の「塔」の代数構造を分解しました。例として、モノイドを指定するには、最初に半グループを定義し、Agda標準ライブラリと同じパターンに従って、monoid定義を使用する可換性モノイドを定義します。

私のトラブルは、私は別の1つの中の深いです代数構造（CommutativeSemiringの一部であるMonoidの例えばプロパティ）のプロパティを必要とするとき、我々は必要な代数構造に等しい突起の数を使用する必要があるということです深さ私の問題の一例として、

、以下の「補題」を検討：モノイドの左側のIDプロパティにアクセスするために、私は内でモノイドからそれを投影する必要があることに注意

open import Algebra 
open import Algebra.Structures 
open import Data.Vec 
open import Relation.Binary.PropositionalEquality 
open import Algebra.FunctionProperties 
open import Data.Product 

module _ {Carrier : Set} {_+_ _*_ : Op₂ Carrier} {0# 1# : Carrier} (ICSR : IsCommutativeSemiring _≡_ _+_ _*_ 0# 1#) where 

csr : CommutativeSemiring _ _ 
csr = record{ isCommutativeSemiring = ICSR } 

zipWith-replicate-0# : ∀ {n}(xs : Vec Carrier n) → zipWith _+_ (replicate 0#) xs ≡ xs 
zipWith-replicate-0# [] = refl 
zipWith-replicate-0# (x ∷ xs) = cong₂ _∷_ (proj₁ (IsMonoid.identity (IsCommutativeMonoid.isMonoid 
                  (IsCommutativeSemiring.+-isCommutativeMonoid 
                  (CommutativeSemiring.isCommutativeSemiring csr)))) x) 
              (zipWith-replicate-0# xs) 

を交換可能なモノイドは交換可能なセミリーディングの構造にあります。

私が懸念しているのは、ますます多くの代数構造を追加すると、そのような補題は読めなくなるということです。

私の質問です：記録投影のこの「はしご」を避けるパターンやトリックはありますか？

これに関する手掛かりは大変歓迎します。

Answer 1

Agda標準ライブラリを見ると、最も特化した代数構造の場合、それらを定義するrecordは、より特殊化されていない構造open publicを持つことがわかります。例えば。 Algebra.AbelianGroupに、我々は持っている：

record AbelianGroup c ℓ : Set (suc (c ⊔ ℓ)) where 
    -- ... snip ... 

    open IsAbelianGroup isAbelianGroup public 

    group : Group _ _ 
    group = record { isGroup = isGroup } 

    open Group group public using (setoid; semigroup; monoid; rawMonoid) 

    -- ... snip ...  

のでAbelianGroupレコードがGroupからだけではなくAbelianGroup/IsAbelianGroup利用可能なフィールドが、また、setoid、semigroupとmonoidとrawMonoidを持つことになります。同様に、setoid,monoidおよびrawMonoidのGroupから同様にopen public - これらのフィールドをMonoidから送信します。

同様に、代数プロパティーの目撃者の場合、専門化されていないバージョンのフィールドを再エクスポートします。 IsAbelianGroupに我々は

record IsAbelianGroup 
     {a ℓ} {A : Set a} (≈ : Rel A ℓ) 
     (∙ : Op₂ A) (ε : A) (⁻¹ : Op₁ A) : Set (a ⊔ ℓ) where 
    -- ... snip ... 
    open IsGroup isGroup public 
    -- ... snip ... 

、その後IsGroup再輸出IsMonoid、IsMonoid再輸出IsSemigroup、などがあります。したがって、もしあなたがIsAbelianGroupを開いていれば、手全体のパスを書き出すことなく、assoc（IsSemigroupから）を使うことができます。

一番下の行は次のように、あなたの関数を書くことができます：

open CommutativeSemiring CSR hiding (refl) 
open import Function using (_⟨_⟩_) 

zipWith-replicate-0# : ∀ {n}(xs : Vec Carrier n) → zipWith _+_ (replicate 0#) xs ≡ xs 
zipWith-replicate-0# [] = refl 
zipWith-replicate-0# (x ∷ xs) = proj₁ +-identity x ⟨ cong₂ _∷_ ⟩ zipWith-replicate-0# xs