Simpler proof of Isomorphism.≲-antisym

[peterthiemann]

I was surprised to discover that the proof of Isomorphism.≲-antisym can be simplified.
Here is the original proof:

plfa.github.io/src/plfa/part1/Isomorphism.lagda.md

Lines 397 to 421 in 8e5406e

	```agda
	≲-antisym : ∀ {A B : Set}
	→ (A≲B : A ≲ B)
	→ (B≲A : B ≲ A)
	→ (to A≲B ≡ from B≲A)
	→ (from A≲B ≡ to B≲A)
	-------------------
	→ A ≃ B
	≲-antisym A≲B B≲A to≡from from≡to =
	record
	{ to = to A≲B
	; from = from A≲B
	; from∘to = from∘to A≲B
	; to∘from = λ{y →
	begin
	to A≲B (from A≲B y)
	≡⟨ cong (to A≲B) (cong-app from≡to y) ⟩
	to A≲B (to B≲A y)
	≡⟨ cong-app to≡from (to B≲A y) ⟩
	from B≲A (to B≲A y)
	≡⟨ from∘to B≲A y ⟩
	y
	∎}
	}
	```

Interestingly, one can pattern match against the arguments to≡from and from≡to resulting in this shorter proof:

≲-antisym A≲B B≲A to≡from@refl from≡to@refl =
  record
    { to      = to A≲B
    ; from    = from A≲B
    ; from∘to = from∘to A≲B
    ; to∘from = from∘to B≲A
    }

Matching against refl works only because records are subject to eta-expansion.
What is the argument for having the longer proof in the text?

[wadler]

Neatly observed! Like you, I'm surprised this works. Please put in a pull request to update the proof. The pull request should include text to add to PLFA to explain to its readers the lesson they should take from the example. I think you are in a better place than me to extract the lesson, but one possible lesson is this: pattern match against refl when you can, and be aware of how eta expansion can make this possible when otherwise it might not work.

[peterthiemann]

Do you want me to replace the current proof or discuss the direct matching version as an alternative?