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

[Fredrik Nordvall Forsberg]

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.

-- 
Fredrik Nordvall Forsberg,
Department of Computer and Information Sciences, University of Strathclyde.
The University of Strathclyde is a charitable body, registered in Scotland, with registration number SC015263.