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

[Alan Jeffrey]

I've given it a bit of a shot, but didn't get very far. Does J follow 
from univalence?

On 02/02/2015 08:49 AM, Andrea Vezzosi wrote:
> Have you tried to implement J for ≡₁, and check how it computes?
>
>
> On Fri, Jan 23, 2015 at 11:53 PM, Alan Jeffrey <ajeffrey at bell-labs.com> wrote:
>> Hi all,
>>
>> OK, I made another shot at a computational version of univalence, using
>> Agda's primTrustMe to get beta-reduction.
>>
>> In the attached Agda code, there's a construction of the 2-categorical
>> version of univalence such that many of the equivalences are
>> beta-reductions. In particular:
>>
>>    ap(ua(e))(a)  beta reduces to  e(a)
>>
>> I only did the 2-categorical version, which lifts up the skeletal
>> equivalence on Set_0 to a non-skeletal equivalence on Set_1. It would be
>> interesting to see if it goes through for any Set_n, to get an n-categorical
>> model, but this may require more book-keeping than I am capable of.
>>
>> Let ≣ be the skeletal equivalence satisfying K.
>>
>> The identity type on Set₀ is (a ≡₀ b) whenever (a ≣ b). From this, we can
>> define (A ≃₁ B : Set₀) as per usual (half-adjoint equivalences).
>>
>> The definition of the identity type on Set₁ is (a ≡₁ b : A) whenever:
>>
>> - p : (a ≣ b)
>> - q : ∀ C → (C a ≃₁ C b)
>> - r : ∀ C D → (q (C ∘ D)) ≣ (≃₁-cong C (q D))
>>
>> from which we can define (A ≃₂ B : Set₁), and show the 2-categorical version
>> of univalence:
>>
>>    (A ≡₁ B) ≃₂ (A ≃₁ B)
>>
>> The Agda trick to getting beta-reductions is that from:
>>
>>    trustMe : ∀ (a b : A) → (a ≣ b)
>>
>> we can build:
>>
>>    POSTULATE[_↦_] : ∀ (a : A) (b : B a) → (∀ a → B a)
>>    POSTULATE[ a ↦ b ] a′ with trustMe a a′
>>    POSTULATE[ a ↦ b ] .a | refl = b
>>
>> Since trustMe a a beta-reduces to refl, (POSTULATE[ a ↦ b ] a) beta-reduces
>> to b. We can use this to make some of the coherence conditions definitional
>> equalities, not just propositional ones. For example, the congruence
>> property for equivalence can be defined:
>>
>>    ≃₁-cong : ∀ {A B} C → (A ≃₁ B) → (C A ≃₁ C B)
>>    ≃₁-cong = POSTULATE[ id ↦ id ]
>>
>> which means that (≃₁-cong id e) beta-reduces to e. From this, we get that
>> ap(ua(e))(a) beta reduces to e(a).
>>
>> One restriction is that the only beta-reduction on postulates is the one
>> given. This is good because we can't introduce nondeterminism, but bad
>> because we only get one beta-reduction per term, so we have to choose
>> carefully which propositional equality to make definitional.
>>
>> Thoughts? Is the construction of ≡₁ as a contextual equivalence generated by
>> ≃₁ new?
>>
>> 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.
>