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

[Alan Jeffrey]

Thanks!

On 02/03/2015 02:45 AM, Andrea Vezzosi wrote:
> It does if you can prove that (x , refl) ≡₁ (y , eq) for every eq : x
> ≡₁ y and fill the hole below:
>
> J : ∀ {A} {x : A} (P : ∃ (\ (y : A) → x ≡₁ y) → Set _) → P (x ,
> ≡₁-refl) → ∀ {y} → (eq : x ≡₁ y) → P (y , eq)
> J P p eq = ap₁ (≡₁-cong P ?) p
>
> On Mon, Feb 2, 2015 at 4:42 PM, Alan Jeffrey <ajeffrey at bell-labs.com> wrote:
>> 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.
>>>
>>>
>>
>