[Agda] Re: [HoTT] Re: Univalence via Agda's primTrustMe again^2

[Alan Jeffrey]

Yes, it's a bit surprising that univalence holds without requiring any 
extra structure, in particular there's no postulate saying that cong 
distributes through either function composition or transitivity of ≃.

If cong distributes through function composition, then in particular 
when F : Set -> Set is an equivalence, then

   cong F⁻¹ (cong F e) = cong (F⁻¹ o F) e = cong id e = e

so (cong F e) must in some sense be preserving e through F. This is a 
bit unsatisfactory though, as it's not saying how e is being preserved. 
In particular, if F is a functor, then (apply (cong F e)) should be the 
same as (map (apply e)).

A.

On 02/18/2015 07:24 PM, Andrea Vezzosi wrote:
> It seems like we'd like more things to hold for cong, cong F e should
> be equal to some equivalence which "lifts" e through F.
>
> The issue is that F is not carrying any description of how to do that,
> which is where these simplicial/cubical models come into play.
>
> Cheers,
> Andrea
>
> On Thu, Feb 19, 2015 at 1:04 AM, Alan Jeffrey <ajeffrey at bell-labs.com> wrote:
>> Sorry for the spam...
>>
>> I managed to prove what were previously postulates. The remaining postulates
>> are J, and the congruence rule for ≃. Univalence follows from these, using
>> the inductive definition of ≡.
>>
>> I am a bit surprised by this, am I missing something?
>>
>> A.
>>
>>
>> On 02/17/2015 12:02 PM, Alan Jeffrey wrote:
>>>
>>> Hi everyone,
>>>
>>> Here is a very tidied up version of how Agda's primTrustMe can be used
>>> to define a model in which univalence holds...
>>>
>>> The idea is to define equivalence and identity types by induction of
>>> universe level. At level n, (A ≃ B) is the usual definition of
>>> half-adjoint equivalence, which uses ≡ at level n. At level 0, (a ≡ b)
>>> is just skeletal propositional equality. At level n+1, (a ≡ b) is
>>> defined to be ∀ F → (F a ≃ F b).
>>>
>>> We can postulate J, with its beta reduction rule (using Agda's
>>> primTrustMe to define postulates with beta-reductions).
>>>
>>> Part of univalence is postulating that ≃ is a congruence, that is there
>>> is a term cong F : (A ≃ B) → (F A ≃ F B). Somewhat annoyingly, this has
>>> two obvious beta-reductions:
>>>
>>>     (cong F refl)  -->  refl
>>>       (cong id p)  -->  p
>>>
>>> Agda doesn't allow such nondeterminism, so in the Agda development I
>>> introduced two congruence rules, cong and cong′. From cong, we can
>>> define ua (and ditto ua′) as:
>>>
>>>     ua : (A ≃ B) -> (A ≡ B)
>>>     ua p F = cong F p
>>>
>>> These have inverses, with type:
>>>
>>>     ua⁻¹ : (A ≡ B) -> (A ≃ B)
>>>
>>> The inverse of ua is the usual extension of the identity function using
>>> J. The invrse of ua′ is:
>>>
>>>     ua′⁻¹ p = p id
>>>
>>> and we can check that ua′⁻¹ (ua′ e) beta reduces to e. To get
>>> univalence, we postulate that ua and ua′ are equivalent, that ua⁻¹ and
>>> ua′⁻¹ are equivalent, and a beta-reduction saying that everything
>>> collapses on reflexivity:
>>>
>>>     ua≡ua′ : ∀ e → (ua n e ≡ ua′ n e)
>>>     ua⁻¹≡ua′⁻¹-cong : (p ≡ q) → (ua⁻¹ n p ≡ ua′⁻¹ n q)
>>>     (ua⁻¹≡ua′⁻¹-cong (ua≡ua′ (ua⁻¹ refl)))  -->  refl
>>>
>>>   From these, we get univalence.
>>>
>>> All comments welcome...
>>>
>>> Alan.
>>
>>
>> --
>> You received this message because you are subscribed to the Google Groups
>> "Homotopy Type Theory" group.
>> To unsubscribe from this group and stop receiving emails from it, send an
>> email to HomotopyTypeTheory+unsubscribe at googlegroups.com.
>> For more options, visit https://groups.google.com/d/optout.