* Re: [HoTT] weak univalence with "beta" implies full univalence
2016-09-07 15:10 weak univalence with "beta" implies full univalence Dan Licata
@ 2016-09-07 16:10 ` Andrew Pitts
2016-09-07 22:20 ` Dan Licata
2016-09-07 17:50 ` Michael Shulman
` (2 subsequent siblings)
3 siblings, 1 reply; 9+ messages in thread
From: Andrew Pitts @ 2016-09-07 16:10 UTC (permalink / raw)
To: Dan Licata; +Cc: Homotopy Type Theory, Prof. Andrew M Pitts
On 7 September 2016 at 16:10, Dan Licata <d...@cs.cmu.edu> wrote:
> What I’m about to say is a trivial consequence of an observation that Egbert/Martin made a couple of years ago (https://github.com/HoTT/book/issues/718), so maybe other people have already realized this, but it was surprising to me.
Very spooky: I recently noticed this for myself (though not via the
observation you mention) and was just about to ask this list whether
it was "well known".
> In particular, based on Martin’s observation https://github.com/HoTT/book/issues/718#issuecomment-65378867
> that any retraction of an identity type is an equivalence:
>
> retract-of-Id-is-Id : ∀ {A : Set} {R : A → A → Set} →
> (r : {x y : A} → x == y -> R x y)
> (s : {x y : A} → R x y → x == y)
> (comp1 : {x y : A} (c : R x y) → r (s c) == c)
> → {x y : A} → IsEquiv {x == y} {R x y} (r {x}{y})
>
> it is enough to assert “ua” (equivalence to path) and the “beta” direction of the full univalence axiom, i.e. the fact that transporting along such a path is the equivalence:
>
> ua : ∀ {A B} → Equiv A B → A == B
> uaβ : ∀ {A B} (e : Equiv A B) → transport (\ X -> X) (ua e) == fst e
>
> The “eta” direction comes for free by Martin’s argument.
You are stating this for the usual inductively defined Martin-Lof
identity type ==, right? Actually I believe it holds with respect to
any notion of propositional identity type (by which I mean any model
of the Coquand-Danielsson axioms), such as the path types that occur
in the CCHM model. Also I think you need to assume the identity types,
whatever they are, satisfy function extensionality don't you?
> Unless the absence of definitional beta reduction for J somehow gets in the way,
I don't think it does get in the way.
> I think this gives another arugment why the Glue type in the Cohen,Coquand,Huber,Mortberg cubical type theory gives full univalence: the only thing specifc to cubical type theory that you need to check is that ua and uaβ can be derived from Glue, and the rest of the argument can happen in book HoTT. This is a small simplification/rearrangement of the argument in Appendix B of their paper, essentially saying that condition (3) of Lemma 25 can be replaced by the retraction lemma.
Yes indeed. This certainly seems a pleasantly minimal condition to
have to check for univalence and, as you say, applies to the model of
Cohen,Coquand,Huber & Mortberg [CCHM]. (Ian Orton and I are trying to
apply it to a different model we are developing.)
Andy
^ permalink raw reply [flat|nested] 9+ messages in thread
* Re: [HoTT] weak univalence with "beta" implies full univalence
2016-09-07 16:10 ` [HoTT] " Andrew Pitts
@ 2016-09-07 22:20 ` Dan Licata
2016-09-08 7:59 ` Andrew Pitts
0 siblings, 1 reply; 9+ messages in thread
From: Dan Licata @ 2016-09-07 22:20 UTC (permalink / raw)
To: Andrew Pitts; +Cc: Homotopy Type Theory
Hi Andy,
Thanks for the interesting comments! A few replies below.
>> In particular, based on Martin’s observation https://github.com/HoTT/book/issues/718#issuecomment-65378867
>> that any retraction of an identity type is an equivalence:
>>
>> retract-of-Id-is-Id : ∀ {A : Set} {R : A → A → Set} →
>> (r : {x y : A} → x == y -> R x y)
>> (s : {x y : A} → R x y → x == y)
>> (comp1 : {x y : A} (c : R x y) → r (s c) == c)
>> → {x y : A} → IsEquiv {x == y} {R x y} (r {x}{y})
>>
>> it is enough to assert “ua” (equivalence to path) and the “beta” direction of the full univalence axiom, i.e. the fact that transporting along such a path is the equivalence:
>>
>> ua : ∀ {A B} → Equiv A B → A == B
>> uaβ : ∀ {A B} (e : Equiv A B) → transport (\ X -> X) (ua e) == fst e
>>
>> The “eta” direction comes for free by Martin’s argument.
>
> You are stating this for the usual inductively defined Martin-Lof
> identity type ==, right?
Yes.
> Also I think you need to assume the identity types,
> whatever they are, satisfy function extensionality don't you?
I didn’t, but I stated uaβ as an equation at function type. If it were pointwise, then I would have needed it. For an identity type with definitional J-on-refl reduction, this suffices to get the usual statement of univalence (I updated the file a little to remove a use a funext to make sure). Maybe this depends on having definitional J-on-refl though.
-Dan
^ permalink raw reply [flat|nested] 9+ messages in thread
* Re: [HoTT] weak univalence with "beta" implies full univalence
2016-09-07 22:20 ` Dan Licata
@ 2016-09-08 7:59 ` Andrew Pitts
0 siblings, 0 replies; 9+ messages in thread
From: Andrew Pitts @ 2016-09-08 7:59 UTC (permalink / raw)
To: Dan Licata; +Cc: Homotopy Type Theory, Prof. Andrew M Pitts
On 7 September 2016 at 23:20, Dan Licata <d...@cs.cmu.edu> wrote:
>> Also I think you need to assume the identity types,
>> whatever they are, satisfy function extensionality don't you?
>
> I didn’t, but I stated uaβ as an equation at function type. If it were pointwise, then I would have needed it. For an identity type with definitional J-on-refl reduction, this suffices to get the usual statement of univalence (I updated the file a little to remove a use a funext to make sure). Maybe this depends on having definitional J-on-refl though.
OK, I see. The proof I made up for myself used along the way the fact
that being contractible is a mere proposition; and for that I seemed
to need function extensionality. But in any case, stating uaβ
pointwise seems more useful. Plus the fact that in the models where we
have been using this nice characterisation of univalence, function
extensionality holds for the propositional identity types in question
for other reasons to do with them being given by paths, as you know.
Best wishes,
Andy
^ permalink raw reply [flat|nested] 9+ messages in thread
* Re: [HoTT] weak univalence with "beta" implies full univalence
2016-09-07 15:10 weak univalence with "beta" implies full univalence Dan Licata
2016-09-07 16:10 ` [HoTT] " Andrew Pitts
@ 2016-09-07 17:50 ` Michael Shulman
2016-09-15 17:35 ` Anders
2017-02-28 16:33 ` Ian Orton
3 siblings, 0 replies; 9+ messages in thread
From: Michael Shulman @ 2016-09-07 17:50 UTC (permalink / raw)
To: Dan Licata; +Cc: Homotopy Type Theory
I feel like we sort of knew this, but I'm not sure it was written down
exactly. Essentially the same argument did come up a couple of years
ago in discussing higher inductive-recursive universes:
https://homotopytypetheory.org/2014/06/08/hiru-tdd/
On Wed, Sep 7, 2016 at 8:10 AM, Dan Licata <d...@cs.cmu.edu> wrote:
> Hi,
>
> What I’m about to say is a trivial consequence of an observation that Egbert/Martin made a couple of years ago (https://github.com/HoTT/book/issues/718), so maybe other people have already realized this, but it was surprising to me.
>
> In particular, based on Martin’s observation https://github.com/HoTT/book/issues/718#issuecomment-65378867
> that any retraction of an identity type is an equivalence:
>
> retract-of-Id-is-Id : ∀ {A : Set} {R : A → A → Set} →
> (r : {x y : A} → x == y -> R x y)
> (s : {x y : A} → R x y → x == y)
> (comp1 : {x y : A} (c : R x y) → r (s c) == c)
> → {x y : A} → IsEquiv {x == y} {R x y} (r {x}{y})
>
> it is enough to assert “ua” (equivalence to path) and the “beta” direction of the full univalence axiom, i.e. the fact that transporting along such a path is the equivalence:
>
> ua : ∀ {A B} → Equiv A B → A == B
> uaβ : ∀ {A B} (e : Equiv A B) → transport (\ X -> X) (ua e) == fst e
>
> The “eta” direction comes for free by Martin’s argument.
>
> Here is a self-contained Agda file that checks this:
> https://github.com/dlicata335/hott-agda/blob/master/misc/UABetaOnly-SelfContained.agda
> (Almost all of the file is boilerplate, but I wanted to make sure I wasn’t accidentally using anything from my library that relies on univalence.)
>
> Unless the absence of definitional beta reduction for J somehow gets in the way, I think this gives another arugment why the Glue type in the Cohen,Coquand,Huber,Mortberg cubical type theory gives full univalence: the only thing specifc to cubical type theory that you need to check is that ua and uaβ can be derived from Glue, and the rest of the argument can happen in book HoTT. This is a small simplification/rearrangement of the argument in Appendix B of their paper, essentially saying that condition (3) of Lemma 25 can be replaced by the retraction lemma.
>
> -Dan
>
> --
> 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 HomotopyTypeThe...@googlegroups.com.
> For more options, visit https://groups.google.com/d/optout.
^ permalink raw reply [flat|nested] 9+ messages in thread
* Re: [HoTT] weak univalence with "beta" implies full univalence
2016-09-07 15:10 weak univalence with "beta" implies full univalence Dan Licata
2016-09-07 16:10 ` [HoTT] " Andrew Pitts
2016-09-07 17:50 ` Michael Shulman
@ 2016-09-15 17:35 ` Anders
2016-09-15 19:39 ` Martin Escardo
2017-02-28 16:33 ` Ian Orton
3 siblings, 1 reply; 9+ messages in thread
From: Anders @ 2016-09-15 17:35 UTC (permalink / raw)
To: Dan Licata; +Cc: Homotopy Type Theory
Hi,
I've formalized this in cubicaltt now, a self-contained formalization
can be found here:
https://github.com/mortberg/cubicaltt/blob/master/experiments/univalence_dan.ctt#L123
The proof is a little different from Dan's and follows a sketch that I
got from Thierry:
We have that
ua + uabeta
implies that Equiv A B is a retract of Path U A B. Hence
(X:U) x Equiv A X is a retract of (X:U) x Path U A X
But (X:U) x Path U A X is contractible (contractibility of
singletons). So (X:U) x Equiv A X is contractible as it is a
retraction of a contractible type. This is an alternative formulation
of the univalence axiom as noted by Martín:
https://groups.google.com/forum/#!msg/homotopytypetheory/HfCB_b-PNEU/Ibb48LvUMeUJ
One difference with Dan's proof is that this is not using the "grad
lemma" (if f has a quasi-inverse then it is an equivalence (called
"improve" in Dan's code)). It also shows that not having the
computation rule for J definitionally doesn't get in the way, however
having it would have made the proof of uabeta trivial (I now have to
do some work by hand as two transports don't disappear).
--
Anders
On Wed, Sep 7, 2016 at 11:10 AM, Dan Licata <d...@cs.cmu.edu> wrote:
> Hi,
>
> What I’m about to say is a trivial consequence of an observation that Egbert/Martin made a couple of years ago (https://github.com/HoTT/book/issues/718), so maybe other people have already realized this, but it was surprising to me.
>
> In particular, based on Martin’s observation https://github.com/HoTT/book/issues/718#issuecomment-65378867
> that any retraction of an identity type is an equivalence:
>
> retract-of-Id-is-Id : ∀ {A : Set} {R : A → A → Set} →
> (r : {x y : A} → x == y -> R x y)
> (s : {x y : A} → R x y → x == y)
> (comp1 : {x y : A} (c : R x y) → r (s c) == c)
> → {x y : A} → IsEquiv {x == y} {R x y} (r {x}{y})
>
> it is enough to assert “ua” (equivalence to path) and the “beta” direction of the full univalence axiom, i.e. the fact that transporting along such a path is the equivalence:
>
> ua : ∀ {A B} → Equiv A B → A == B
> uaβ : ∀ {A B} (e : Equiv A B) → transport (\ X -> X) (ua e) == fst e
>
> The “eta” direction comes for free by Martin’s argument.
>
> Here is a self-contained Agda file that checks this:
> https://github.com/dlicata335/hott-agda/blob/master/misc/UABetaOnly-SelfContained.agda
> (Almost all of the file is boilerplate, but I wanted to make sure I wasn’t accidentally using anything from my library that relies on univalence.)
>
> Unless the absence of definitional beta reduction for J somehow gets in the way, I think this gives another arugment why the Glue type in the Cohen,Coquand,Huber,Mortberg cubical type theory gives full univalence: the only thing specifc to cubical type theory that you need to check is that ua and uaβ can be derived from Glue, and the rest of the argument can happen in book HoTT. This is a small simplification/rearrangement of the argument in Appendix B of their paper, essentially saying that condition (3) of Lemma 25 can be replaced by the retraction lemma.
>
> -Dan
>
> --
> 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 HomotopyTypeThe...@googlegroups.com.
> For more options, visit https://groups.google.com/d/optout.
^ permalink raw reply [flat|nested] 9+ messages in thread
* Re: [HoTT] weak univalence with "beta" implies full univalence
2016-09-15 17:35 ` Anders
@ 2016-09-15 19:39 ` Martin Escardo
2016-10-17 0:58 ` Jason Gross
0 siblings, 1 reply; 9+ messages in thread
From: Martin Escardo @ 2016-09-15 19:39 UTC (permalink / raw)
To: Homotopy Type Theory
Nice, Dan and Anders and Thierry. Martin
On 15/09/16 18:35, Anders wrote:
> Hi,
>
> I've formalized this in cubicaltt now, a self-contained formalization
> can be found here:
>
> https://github.com/mortberg/cubicaltt/blob/master/experiments/univalence_dan.ctt#L123
>
> The proof is a little different from Dan's and follows a sketch that I
> got from Thierry:
>
> We have that
>
> ua + uabeta
>
> implies that Equiv A B is a retract of Path U A B. Hence
>
> (X:U) x Equiv A X is a retract of (X:U) x Path U A X
>
> But (X:U) x Path U A X is contractible (contractibility of
> singletons). So (X:U) x Equiv A X is contractible as it is a
> retraction of a contractible type. This is an alternative formulation
> of the univalence axiom as noted by Martín:
>
> https://groups.google.com/forum/#!msg/homotopytypetheory/HfCB_b-PNEU/Ibb48LvUMeUJ
>
>
> One difference with Dan's proof is that this is not using the "grad
> lemma" (if f has a quasi-inverse then it is an equivalence (called
> "improve" in Dan's code)). It also shows that not having the
> computation rule for J definitionally doesn't get in the way, however
> having it would have made the proof of uabeta trivial (I now have to
> do some work by hand as two transports don't disappear).
>
> --
> Anders
>
> On Wed, Sep 7, 2016 at 11:10 AM, Dan Licata <d...@cs.cmu.edu> wrote:
>> Hi,
>>
>> What I’m about to say is a trivial consequence of an observation that Egbert/Martin made a couple of years ago (https://github.com/HoTT/book/issues/718), so maybe other people have already realized this, but it was surprising to me.
>>
>> In particular, based on Martin’s observation https://github.com/HoTT/book/issues/718#issuecomment-65378867
>> that any retraction of an identity type is an equivalence:
>>
>> retract-of-Id-is-Id : ∀ {A : Set} {R : A → A → Set} →
>> (r : {x y : A} → x == y -> R x y)
>> (s : {x y : A} → R x y → x == y)
>> (comp1 : {x y : A} (c : R x y) → r (s c) == c)
>> → {x y : A} → IsEquiv {x == y} {R x y} (r {x}{y})
>>
>> it is enough to assert “ua” (equivalence to path) and the “beta” direction of the full univalence axiom, i.e. the fact that transporting along such a path is the equivalence:
>>
>> ua : ∀ {A B} → Equiv A B → A == B
>> uaβ : ∀ {A B} (e : Equiv A B) → transport (\ X -> X) (ua e) == fst e
>>
>> The “eta” direction comes for free by Martin’s argument.
>>
>> Here is a self-contained Agda file that checks this:
>> https://github.com/dlicata335/hott-agda/blob/master/misc/UABetaOnly-SelfContained.agda
>> (Almost all of the file is boilerplate, but I wanted to make sure I wasn’t accidentally using anything from my library that relies on univalence.)
>>
>> Unless the absence of definitional beta reduction for J somehow gets in the way, I think this gives another arugment why the Glue type in the Cohen,Coquand,Huber,Mortberg cubical type theory gives full univalence: the only thing specifc to cubical type theory that you need to check is that ua and uaβ can be derived from Glue, and the rest of the argument can happen in book HoTT. This is a small simplification/rearrangement of the argument in Appendix B of their paper, essentially saying that condition (3) of Lemma 25 can be replaced by the retraction lemma.
>>
>> -Dan
>>
>> --
>> 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 HomotopyTypeThe...@googlegroups.com.
>> For more options, visit https://groups.google.com/d/optout.
>
^ permalink raw reply [flat|nested] 9+ messages in thread
* Re: [HoTT] weak univalence with "beta" implies full univalence
2016-09-15 19:39 ` Martin Escardo
@ 2016-10-17 0:58 ` Jason Gross
0 siblings, 0 replies; 9+ messages in thread
From: Jason Gross @ 2016-10-17 0:58 UTC (permalink / raw)
To: Martin Escardo, Homotopy Type Theory
[-- Attachment #1: Type: text/plain, Size: 5183 bytes --]
To belatedly add a little bit to this discussion:
> so maybe other people have already realized this, but it was surprising
to me
A way that I've found to make this seem more obvious is that too use the
encode-decode method, you provide a proof of "forall x, Contr { y : A &
code x y }" (using Coq notation for sigma types). With a bit of
rearranging, giving your ua and uaβ is the same as giving the data for
"forall A (p q : { B : Type & A <~> B }), p = q", i.e., giving the hProp
obligation for contractibility. There's some Coq code that implements this
that I put here:
https://github.com/HoTT/HoTT/issues/757#issuecomment-102128029, and in the
following discussion, Mike and Vladimir and Steve pointed out that this had
been seen before.
-Jason
On Thu, Sep 15, 2016 at 3:39 PM 'Martin Escardo' via Homotopy Type Theory <
HomotopyT...@googlegroups.com> wrote:
> Nice, Dan and Anders and Thierry. Martin
>
> On 15/09/16 18:35, Anders wrote:
> > Hi,
> >
> > I've formalized this in cubicaltt now, a self-contained formalization
> > can be found here:
> >
> >
> https://github.com/mortberg/cubicaltt/blob/master/experiments/univalence_dan.ctt#L123
> >
> > The proof is a little different from Dan's and follows a sketch that I
> > got from Thierry:
> >
> > We have that
> >
> > ua + uabeta
> >
> > implies that Equiv A B is a retract of Path U A B. Hence
> >
> > (X:U) x Equiv A X is a retract of (X:U) x Path U A X
> >
> > But (X:U) x Path U A X is contractible (contractibility of
> > singletons). So (X:U) x Equiv A X is contractible as it is a
> > retraction of a contractible type. This is an alternative formulation
> > of the univalence axiom as noted by Martín:
> >
> >
> https://groups.google.com/forum/#!msg/homotopytypetheory/HfCB_b-PNEU/Ibb48LvUMeUJ
> >
> >
> > One difference with Dan's proof is that this is not using the "grad
> > lemma" (if f has a quasi-inverse then it is an equivalence (called
> > "improve" in Dan's code)). It also shows that not having the
> > computation rule for J definitionally doesn't get in the way, however
> > having it would have made the proof of uabeta trivial (I now have to
> > do some work by hand as two transports don't disappear).
> >
> > --
> > Anders
> >
> > On Wed, Sep 7, 2016 at 11:10 AM, Dan Licata <d...@cs.cmu.edu> wrote:
> >> Hi,
> >>
> >> What I’m about to say is a trivial consequence of an observation that
> Egbert/Martin made a couple of years ago (
> https://github.com/HoTT/book/issues/718), so maybe other people have
> already realized this, but it was surprising to me.
> >>
> >> In particular, based on Martin’s observation
> https://github.com/HoTT/book/issues/718#issuecomment-65378867
> >> that any retraction of an identity type is an equivalence:
> >>
> >> retract-of-Id-is-Id : ∀ {A : Set} {R : A → A → Set} →
> >> (r : {x y : A} → x == y -> R x y)
> >> (s : {x y : A} → R x y → x == y)
> >> (comp1 : {x y : A} (c : R x y) → r (s c) == c)
> >> → {x y : A} → IsEquiv {x == y} {R x y} (r {x}{y})
> >>
> >> it is enough to assert “ua” (equivalence to path) and the “beta”
> direction of the full univalence axiom, i.e. the fact that transporting
> along such a path is the equivalence:
> >>
> >> ua : ∀ {A B} → Equiv A B → A == B
> >> uaβ : ∀ {A B} (e : Equiv A B) → transport (\ X -> X) (ua e) == fst e
> >>
> >> The “eta” direction comes for free by Martin’s argument.
> >>
> >> Here is a self-contained Agda file that checks this:
> >>
> https://github.com/dlicata335/hott-agda/blob/master/misc/UABetaOnly-SelfContained.agda
> >> (Almost all of the file is boilerplate, but I wanted to make sure I
> wasn’t accidentally using anything from my library that relies on
> univalence.)
> >>
> >> Unless the absence of definitional beta reduction for J somehow gets in
> the way, I think this gives another arugment why the Glue type in the
> Cohen,Coquand,Huber,Mortberg cubical type theory gives full univalence: the
> only thing specifc to cubical type theory that you need to check is that ua
> and uaβ can be derived from Glue, and the rest of the argument can happen
> in book HoTT. This is a small simplification/rearrangement of the argument
> in Appendix B of their paper, essentially saying that condition (3) of
> Lemma 25 can be replaced by the retraction lemma.
> >>
> >> -Dan
> >>
> >> --
> >> 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 HomotopyTypeThe...@googlegroups.com.
> >> For more options, visit https://groups.google.com/d/optout.
> >
>
> --
> 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 HomotopyTypeThe...@googlegroups.com.
> For more options, visit https://groups.google.com/d/optout.
>
[-- Attachment #2: Type: text/html, Size: 8961 bytes --]
^ permalink raw reply [flat|nested] 9+ messages in thread
* Re: [HoTT] weak univalence with "beta" implies full univalence
2016-09-07 15:10 weak univalence with "beta" implies full univalence Dan Licata
` (2 preceding siblings ...)
2016-09-15 17:35 ` Anders
@ 2017-02-28 16:33 ` Ian Orton
3 siblings, 0 replies; 9+ messages in thread
From: Ian Orton @ 2017-02-28 16:33 UTC (permalink / raw)
To: HomotopyTypeTheory
[-- Attachment #1: Type: text/plain, Size: 5457 bytes --]
Hi all,
I wanted to follow up on Dan's previous observations by suggesting a
different set of axioms which imply those in his email (and hence imply
univalence). I think these are interesting because they're potentially
easier to check in a model - I'll argue that this is the case for
cubical sets/cubical type theory. I've personally found this
decomposition of univalence particularly useful for understanding what's
going on in the cubical sets model.
Firstly, assume funext*. Next, assume two special cases of ua (as
defined in Dan's email), where A B : Set and C : A → B → Set,
unit : A = (Σ[ a ∈ A ] ⊤)
flip : (Σ[ a ∈ A ] Σ[ b ∈ B ] C a b) = (Σ[ b ∈ B ] Σ[ a ∈ A ] C a b)
Finally, assume the following:
contract : isContr A → A = ⊤
Recall that singletons, sing(x) := Σ[ y ∈ A ] x = y, are contractible
and a function f : A --> B is an equivalence if, for every b : B, the
fiber, fib_f(b) := Σ[ a ∈ A ] (f a = b), is contractible.
Now, given an equivalence (f,e) : isEquiv A B, the following calculation
shows how to construct an equality ua(f,e) : A = B
A = Σ[ a ∈ A ] ⊤ -- by unit
= Σ[ a ∈ A ] Σ[ b ∈ B ] (f a = b) -- by contract on sing(f a)
= Σ[ b ∈ B ] Σ[ a ∈ A ] (f a = b) -- by flip
= Σ[ b ∈ B ] ⊤ -- by contract on fib_f(b)
= B -- by unit
Showing uaβ requires the following assumptions (which are in fact
special cases of uaβ):
unitβ : (A : Set) → transport (λ X → X) (unit A) = λ a → (a , tt)
flipβ : {A B : Set}{C : A → B → Set} →
transport (λ X → X) flip = λ{(a , b , c) → (b , a , c)}
So given funext + these 5 assumptions we get univalence.
All of this has been formalised in Agda, and can be found at
http://www.cl.cam.ac.uk/~rio22/agda/axi-univ/UnivArg.html
To understand why this is interesting, consider the cubical sets model.
Funext is easily validated in cubical sets. The axioms unit and flip
arise as special cases of a more general construction: types in cubical
TT are interpreted as presheaves. Given two types Γ ⊢ A B which are
interpreted as isomorphic presheaves (note that this condition is
stronger than being equivalent types in the type theory) then define a
presheaf P(x,i) := A(x) if i =0 or B(x) otherwise. This gives a new type
Γ, i : I ⊢ P which is A when i=0 and B when i=1. This then gives us a
path in the universe from A to B.
To validate contract you need to, given a contractible type Γ ⊢ A,
define a new type Γ, i : I ⊢ C which is A when i=0 and ⊤ when i=1.
Define C to be the partial elements of A with extent i=0.
When i=0 this is isomorphic to A and when i=1 this is isomorphic to ⊤.
We strengthen the isomorphisms at each end to equalities using the
construction in the previous paragraph.
Everything described here is happening in the Glueing construction
currently used to show univalence.
Cheers,
Ian
* You can make do with weaker assumptions, but things are simpler with
funext, and it doesn't seem to cause problems for the purpose of finding
axioms which are easy to check in models. It's very easy to validate
funext in cubical TT/sets and others models I've been looking at with my
supervisor (Andy Pitts).
On 07/09/2016 16:10, Dan Licata wrote:
> Hi,
>
> What I’m about to say is a trivial consequence of an observation that Egbert/Martin made a couple of years ago (https://github.com/HoTT/book/issues/718), so maybe other people have already realized this, but it was surprising to me.
>
> In particular, based on Martin’s observationhttps://github.com/HoTT/book/issues/718#issuecomment-65378867
> that any retraction of an identity type is an equivalence:
>
> retract-of-Id-is-Id : ∀ {A : Set} {R : A → A → Set} →
> (r : {x y : A} → x == y -> R x y)
> (s : {x y : A} → R x y → x == y)
> (comp1 : {x y : A} (c : R x y) → r (s c) == c)
> → {x y : A} → IsEquiv {x == y} {R x y} (r {x}{y})
>
> it is enough to assert “ua” (equivalence to path) and the “beta” direction of the full univalence axiom, i.e. the fact that transporting along such a path is the equivalence:
>
> ua : ∀ {A B} → Equiv A B → A == B
> uaβ : ∀ {A B} (e : Equiv A B) → transport (\ X -> X) (ua e) == fst e
>
> The “eta” direction comes for free by Martin’s argument.
>
> Here is a self-contained Agda file that checks this:
> https://github.com/dlicata335/hott-agda/blob/master/misc/UABetaOnly-SelfContained.agda
> (Almost all of the file is boilerplate, but I wanted to make sure I wasn’t accidentally using anything from my library that relies on univalence.)
>
> Unless the absence of definitional beta reduction for J somehow gets in the way, I think this gives another arugment why the Glue type in the Cohen,Coquand,Huber,Mortberg cubical type theory gives full univalence: the only thing specifc to cubical type theory that you need to check is that ua and uaβ can be derived from Glue, and the rest of the argument can happen in book HoTT. This is a small simplification/rearrangement of the argument in Appendix B of their paper, essentially saying that condition (3) of Lemma 25 can be replaced by the retraction lemma.
>
> -Dan
>
[-- Attachment #2: Type: text/html, Size: 6706 bytes --]
^ permalink raw reply [flat|nested] 9+ messages in thread