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

[Andrea Vezzosi]

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.
>>
>>
>