CODEWITHSUNDEEP
agda
white_wolf
white_wolf

Reputation: 646

Substituting equal term in equality proof

I have the following definition

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

And I'm trying to show transitivity. I have what I need, but I don't know how to combine them to get the proof object I want. This is the proof so far.

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

In the first hole, I have these: (the second hole is identical)

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

Now, it's obvious that if I replace f₁ a with g₂ (f₂ (f₁ a)) in xa I get to the goal. But I don't know how to do this substitution in agda. What kind of function or language construct do I need to do this?

Upvotes: 2

Views: 201

Answers (2)

Cactus
Cactus

Reputation: 27626

You can write it very compactly as

trans xa (cong g₁ wb)

Or, using Function._⟨_⟩_:

xa ⟨ trans ⟩ (cong g₁ wb)

Upvotes: 3

white_wolf
white_wolf

Reputation: 646

I solved it with equational reasoning in the following way:

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)))
                  ∎)

Upvotes: 2

Related Questions