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

[Andrea Vezzosi]

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.