Подставив равный член в равенстве доказательство

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) 

Теперь, очевидно, что, если я заменю f₁ a с g₂ (f₂ (f₁ a)) в xa добраться до цели. Но я не знаю, как сделать эту замену в 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)