[Agda] HoTT-Agda question

[Jacques Carette]

Thanks, that helps a lot.

If I re-interpret your second paragraph, you are saying that which one 
to use depends on intentional aspects: what will the equivalence be use 
for / what context will it be used in, will influence which 
representation works smoothest.

Which I should have seen!  This is exactly why, along with Michael 
Kohlhasse and Bill Farmer, we 'invented' the concept of a Realm [1][2] 
to capture exactly this use case: that certain theories [Equiv is a 
presentation of the theory of equivalences as an "algebraic theory"] 
have multiple equivalent presentations, and that users should be able to 
freely choose the most convenient one, without being forced into 
adopting the one that library developers have chosen.

Jacques

[1] http://link.springer.com/chapter/10.1007/978-3-319-08434-3_19
[2] http://arxiv.org/abs/1405.5956

On 2015-03-11 10:31 AM, Dan Licata wrote:
> 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