Substituer égal terme en matière d'égalité preuve

Question

J'ai la définition suivante

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 

Et je suis en train de montrer transitivité. J'ai ce dont j'ai besoin, mais je ne sais pas comment les combiner pour obtenir l'objet de preuve que je veux. C'est la preuve jusqu'à présent.

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 {!!}) 

Dans le premier trou, j'ai celles-ci: (le deuxième trou est identique)

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

Maintenant, il est évident que si je remplace f₁ a avec g₂ (f₂ (f₁ a)) dans xa je reçois à l'objectif. Mais je ne sais pas comment faire cette substitution dans agda. De quel type de fonction ou de construction de langage ai-je besoin pour faire cela?

Answer 1

Je l'ai résolu avec le raisonnement equational de la manière suivante:

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

Vous pouvez l'écrire très comme compacte

trans xa (cong g₁ wb) 

Ou, en utilisant Function._⟨_⟩_:

xa ⟨ trans ⟩ (cong g₁ wb)