平等に等しい用語を代入証明

Question

私は、次のように定義さ

open import Relation.Binary.PropositionalEquality 

data _≅_ (A B : Set) : Set where 
    mkBij : (f : A → B) (g : B → A) 
      → (∀ a → a ≡ g (f a)) 
      → (∀ b → b ≡ f (g b)) 
      → A ≅ B 

そして、私は推移を表示しようとしているがあります。私は必要なものを持っていますが、それらを組み合わせて私が望むプルーフオブジェクトを得る方法はわかりません。これはこれまでの証明です。最初の穴に

transtv : ∀ {A B C} → A ≅ B → B ≅ C → A ≅ C 
transtv (mkBij f₁ g₁ x y) (mkBij f₂ g₂ w z) = 
    mkBij (λ x₁ → f₂ (f₁ x₁)) (λ z₁ → g₁ (g₂ z₁)) 
     (λ a → let xa = x a 
        wb = w (f₁ a) 
       in {!!}) 
     (λ c → let zc = z c 
        yb = y (g₂ c) 
       in {!!}) 

、私はこれらを持っている：

Goal: a ≡ g₁ (g₂ (f₂ (f₁ a))) 
wb : f₁ a ≡ g₂ (f₂ (f₁ a)) 
xa : a ≡ g₁ (f₁ a) 

今、それは私がxaにg₂ (f₂ (f₁ a))でf₁ aを交換する場合、私はゴールに着くことは明らかです（第2の穴が同一です）。しかし、私はどのようにagdaでこの置換を行うのか分からない。どのような機能や言語の構成が必要ですか？

Answer 1

私は次のように等式推論とそれを解決：

transtv : ∀ {A B C} → A ≅ B → B ≅ C → A ≅ C 
transtv (mkBij f₁ g₁ x y) (mkBij f₂ g₂ w z) = 
    mkBij (λ x₁ → f₂ (f₁ x₁)) (λ z₁ → g₁ (g₂ z₁)) 
     (λ a → let xa = x a 
        wb = w (f₁ a) 
       in begin 
        a 
        ≡⟨ xa ⟩ 
        g₁ (f₁ a) 
        ≡⟨ cong g₁ wb ⟩ 
        g₁ (g₂ (f₂ (f₁ a))) 
        ∎) 
     (λ c → let zc = z c 
        yb = y (g₂ c) 
       in begin 
        c 
        ≡⟨ zc ⟩ 
        f₂ (g₂ c) 
        ≡⟨ cong f₂ yb ⟩ 
        f₂ (f₁ (g₁ (g₂ c))) 
        ∎) 

Answer 2

をあなたは

trans xa (cong g₁ wb) 

または、Function._⟨_⟩_を使用して、非常にコンパクトにそれを書くことができます。

xa ⟨ trans ⟩ (cong g₁ wb)