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

[Alan Jeffrey]

Indeed, we could just postulate J, but it would be nice if this wasn't 
necessary (possibly by changing the defn of ≡₁).

A.

On 02/03/2015 10:17 AM, Fredrik Nordvall Forsberg wrote:
> Hi,
>
>>> 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?
>
> I would be surprised if J followed from univalence. However, the same trick (with a small twist) seems
> to work to define J for ≡₁, with the right computation rule:
>
> J : ∀ {A}(P : (x y : A) -> x ≡₁ y → Set) → ((x : A) -> P x x ≡₁-refl) → (x y : A) → (eq : x ≡₁ y) → P x y eq
> J P d x .x ⟨ ≣-refl , q , r ⟩ = POSTULATE[_↦_] {B = P x x} ≡₁-refl (d x) ⟨ ≣-refl , q , r ⟩
>
> J-comp : ∀ {A}(P : (x y : A) -> x ≡₁ y → Set) → (d : (x : A) -> P x x ≡₁-refl) → (x : A) → (J P d x x ≡₁-refl) ≣ d x
> J-comp P d x = ≣-refl
>
> Best wishes,
> Fredrik
>
> On 03 February 2015 15:42, Alan Jeffrey [ajeffrey at bell-labs.com] wrote:
>> 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.
>