[Agda] HoTT-Agda question

[Dan Licata]

Hi Jacques,

In my agda code for hott, I use a record like you show below.  There are pros and cons.  I agree that it is easier to use the record version.  But if you use an iterated sigma, then you can reuse lemmas for sigmas (e.g. a path in a sigma is a pair of paths, etc.), while if you use a record, then you need to reprove these lemmas for the record type.  In some versions of the library (not sure what's current) I think we had both the record version and the sigma version and an equivalence between the two.

Regarding "why is equivalence oriented?", I agree that often you want to work with the type Equiv A B, rather than the type IsEquiv f.  But sometimes you do want the latter.  For example, to state univalence or function extensionality concisely, there is a particular f that you want to say is an equivalence; you don't just want to postulate an arbitrary equivalence.  Also, IsEquiv f is an hprop, so sometimes it is convenient to massage the goal into proving that some function f is an equivalence, e.g. so that you can eliminate on a -1-truncated type.  

-Dan

On Mar 11, 2015, at 10:15 AM, Jacques Carette <carette at mcmaster.ca> wrote:

> 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
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda