[Agda] HoTT-Agda question

[Jacques Carette]

Equivalences can be defined (as in the HoTT book and elsewhere) using 
the notion of quasi-inverse, usually rendered in Agda as

infix 4 _∼_
infix 4 _≃_

_∼_ : ∀ {ℓ ℓ'} → {A : Set ℓ} {P : A → Set ℓ'} →
       (f g : (x : A) → P x) → Set (ℓ ⊔ ℓ')
f ∼ g = ∀ x → f x ≡ g x

record qinv {ℓ ℓ'} {A : Set ℓ} {B : Set ℓ'} (f : A → B) : Set (ℓ ⊔ ℓ') where
   constructor mkqinv
   field
     g : B → A
     α : (f ∘ g) ∼ id
     β : (g ∘ f) ∼ id

_≃_ : ∀ {ℓ ℓ'} (A : Set ℓ) (B : Set ℓ') → Set (ℓ ⊔ ℓ')
A ≃ B = Σ (A → B) qinv

In practice however, dealing with "elements" of A ≃ B is awkward and 
verbose.  Is it conceptually improper to instead model this as

record _≈_ {ℓ ℓ'} {A : Set ℓ} {B : Set ℓ'} : Set (ℓ ⊔ ℓ') where
   constructor equiv
   field
     f : A → B
     g : B → A
     α : (f ∘ g) ∼ id
     β : (g ∘ f) ∼ id

This is considerably simpler to work with.  And they are equivalent types.

The reason I ask is that, mathematically, these "say" different things: 
the first definition is most definitely oriented (i.e. f : A → B is an 
equivalence between A and B if we are also given the data in qinv), 
while the second is "naturally symmetric" in A and B, as well as in f 
and g, and says that an equivalence is 4 pieces of data, NOT 1+3.  
[Aside: In physics, there is difference between 4 and 3+1, in that 4 
dimensions of spaces are very different from 3 dimensions of space and 1 
dimension of time, even though as 'numbers' these are the same].

I do understand why 'isequiv' (see the HoTT book) is oriented: f does 
play a special role, with g and h being right/left inverses. However, I 
still don't understand why the definition of 'isequiv' is not usually 
encoded as a single record instead of as a Sigma type. Since records, 
qua telescopes, ARE Sigma types, why make it so much harder to 
manipulate them?

Fundamentally, however, I have never understood why the definition of 
equivalence in the HoTT book was 'oriented'.  Especially since, in 
practice, the single-record / symmetric definition is considerably 
easier to work with [where "in practice" = "in Agda"].

Comments?  [And should I be asking here or on the HoTT list?]

Jacques