Weaker forms of univalence

Weaker forms of univalence

[Ian Orton]

Consider the following three statements, for all types A and B:

   (1)  (A ≃ B) -> (A = B)
   (2)  (A ≃ B) ≃ (A = B)
   (3)  isEquiv idtoeqv

(3) is the full univalence axiom and we have implications (3) -> (2) -> 
(1), but can we say anything about the other directions? Do we have (1) 
-> (2) or (2) -> (3)? Can we construct models separating any/all of 
these three statements?

Thanks,
Ian

Re: [HoTT] Weaker forms of univalence

[Michael Shulman]

It was observed previously on this list, I think, that full univalence
(3) is equivalent to

(4)  forall A, IsContr( Sigma(B:U) (A ≃ B) ).

This follows from the fact that a fiberwise map is a fiberwise
equivalence as soon as it induces an equivalence on total spaces, and
the fact that based path spaces are contractible.  But the
contractibility of based path spaces also gives (2) -> (4), and hence
(2) -> (3).

I am not sure about (1).  It might be an open question even in the
case when A and B are propositions.


On Wed, Jul 19, 2017 at 9:26 AM, Ian Orton <ri...@cam.ac.uk> wrote:
> Consider the following three statements, for all types A and B:
>
>   (1)  (A ≃ B) -> (A = B)
>   (2)  (A ≃ B) ≃ (A = B)
>   (3)  isEquiv idtoeqv
>
> (3) is the full univalence axiom and we have implications (3) -> (2) -> (1),
> but can we say anything about the other directions? Do we have (1) -> (2) or
> (2) -> (3)? Can we construct models separating any/all of these three
> statements?
>
> Thanks,
> Ian
>
> --
> 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.

Re: [HoTT] Weaker forms of univalence

[Nicolai Kraus]

On 19/07/17 18:19, Michael Shulman wrote:
> I am not sure about (1).  It might be an open question even in the
> case when A and B are propositions.

If we restrict ourselves to the case that A and B are propositions, then
   (1)  (A ≃ B) -> (A = B)
is as strong as (2) / (3), since (1) then says that equality is implied 
by a reflexive propositional relation and thus a proposition.
Of course this needs funext.
(Afaik (1) is often called "propositional extensionality", but we could 
also just call it "univalence for propositions.)

We have once discussed on this list whether (1) is consistent with UIP 
(i.e. it would be different from (2)), but we did not find an answer.

Nicolai

Re: [HoTT] Weaker forms of univalence

[Bas Spitters]

>It was observed previously on this list,
Maybe we should be using our wiki more?
https://ncatlab.org/homotopytypetheory/


On Wed, Jul 19, 2017 at 7:19 PM, Michael Shulman <shu...@sandiego.edu> wrote:
> It was observed previously on this list, I think, that full univalence
> (3) is equivalent to
>
> (4)  forall A, IsContr( Sigma(B:U) (A ≃ B) ).
>
> This follows from the fact that a fiberwise map is a fiberwise
> equivalence as soon as it induces an equivalence on total spaces, and
> the fact that based path spaces are contractible.  But the
> contractibility of based path spaces also gives (2) -> (4), and hence
> (2) -> (3).
>
> I am not sure about (1).  It might be an open question even in the
> case when A and B are propositions.
>
>
> On Wed, Jul 19, 2017 at 9:26 AM, Ian Orton <ri...@cam.ac.uk> wrote:
>> Consider the following three statements, for all types A and B:
>>
>>   (1)  (A ≃ B) -> (A = B)
>>   (2)  (A ≃ B) ≃ (A = B)
>>   (3)  isEquiv idtoeqv
>>
>> (3) is the full univalence axiom and we have implications (3) -> (2) -> (1),
>> but can we say anything about the other directions? Do we have (1) -> (2) or
>> (2) -> (3)? Can we construct models separating any/all of these three
>> statements?
>>
>> Thanks,
>> Ian
>>
>> --
>> 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.

Re: [HoTT] Weaker forms of univalence

[Steve Awodey]

I think we’ve been through this before:

 (1)  (A ≃ B) -> (A = B)

is logically equivalent to what may be called “invariance”:  

	if P(X) is any type depending on a type variable X, then given any equivalence e : A ≃ B , we have P(A) ≃ P(B).

if we add to this a certain “computation rule”, we get something logically equivalent to UA: 
assume p : A ≃ B → A = B; then given e : A ≃ B, we have p(e) : A = B is a path in U. 
Since we can transport along this path in any family of types over U, and transport is always an equivalence, 
there is a transport p(e)∗ : A ≃ B in the identity family.  
The required “computation rule” states that p(e)∗ = e. 

Steve



> On Jul 20, 2017, at 8:56 AM, Bas Spitters <b.a.w.s...@gmail.com> wrote:
> 
>> It was observed previously on this list,
> Maybe we should be using our wiki more?
> https://ncatlab.org/homotopytypetheory/
> 
> 
> On Wed, Jul 19, 2017 at 7:19 PM, Michael Shulman <shu...@sandiego.edu> wrote:
>> It was observed previously on this list, I think, that full univalence
>> (3) is equivalent to
>> 
>> (4)  forall A, IsContr( Sigma(B:U) (A ≃ B) ).
>> 
>> This follows from the fact that a fiberwise map is a fiberwise
>> equivalence as soon as it induces an equivalence on total spaces, and
>> the fact that based path spaces are contractible.  But the
>> contractibility of based path spaces also gives (2) -> (4), and hence
>> (2) -> (3).
>> 
>> I am not sure about (1).  It might be an open question even in the
>> case when A and B are propositions.
>> 
>> 
>> On Wed, Jul 19, 2017 at 9:26 AM, Ian Orton <ri...@cam.ac.uk> wrote:
>>> Consider the following three statements, for all types A and B:
>>> 
>>>  (1)  (A ≃ B) -> (A = B)
>>>  (2)  (A ≃ B) ≃ (A = B)
>>>  (3)  isEquiv idtoeqv
>>> 
>>> (3) is the full univalence axiom and we have implications (3) -> (2) -> (1),
>>> but can we say anything about the other directions? Do we have (1) -> (2) or
>>> (2) -> (3)? Can we construct models separating any/all of these three
>>> statements?
>>> 
>>> Thanks,
>>> Ian
>>> 
>>> --
>>> 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.
> 
> -- 
> 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.

Re: [HoTT] Weaker forms of univalence

[Michael Shulman]

But is it known that this is definitely weaker?  E.g. are there models
that satisfy invariance but not the computation rule?

On Thu, Jul 20, 2017 at 4:59 AM, Steve Awodey <awo...@cmu.edu> wrote:
> I think we’ve been through this before:
>
>  (1)  (A ≃ B) -> (A = B)
>
> is logically equivalent to what may be called “invariance”:
>
>         if P(X) is any type depending on a type variable X, then given any equivalence e : A ≃ B , we have P(A) ≃ P(B).
>
> if we add to this a certain “computation rule”, we get something logically equivalent to UA:
> assume p : A ≃ B → A = B; then given e : A ≃ B, we have p(e) : A = B is a path in U.
> Since we can transport along this path in any family of types over U, and transport is always an equivalence,
> there is a transport p(e)∗ : A ≃ B in the identity family.
> The required “computation rule” states that p(e)∗ = e.
>
> Steve
>
>
>
>> On Jul 20, 2017, at 8:56 AM, Bas Spitters <b.a.w.s...@gmail.com> wrote:
>>
>>> It was observed previously on this list,
>> Maybe we should be using our wiki more?
>> https://ncatlab.org/homotopytypetheory/
>>
>>
>> On Wed, Jul 19, 2017 at 7:19 PM, Michael Shulman <shu...@sandiego.edu> wrote:
>>> It was observed previously on this list, I think, that full univalence
>>> (3) is equivalent to
>>>
>>> (4)  forall A, IsContr( Sigma(B:U) (A ≃ B) ).
>>>
>>> This follows from the fact that a fiberwise map is a fiberwise
>>> equivalence as soon as it induces an equivalence on total spaces, and
>>> the fact that based path spaces are contractible.  But the
>>> contractibility of based path spaces also gives (2) -> (4), and hence
>>> (2) -> (3).
>>>
>>> I am not sure about (1).  It might be an open question even in the
>>> case when A and B are propositions.
>>>
>>>
>>> On Wed, Jul 19, 2017 at 9:26 AM, Ian Orton <ri...@cam.ac.uk> wrote:
>>>> Consider the following three statements, for all types A and B:
>>>>
>>>>  (1)  (A ≃ B) -> (A = B)
>>>>  (2)  (A ≃ B) ≃ (A = B)
>>>>  (3)  isEquiv idtoeqv
>>>>
>>>> (3) is the full univalence axiom and we have implications (3) -> (2) -> (1),
>>>> but can we say anything about the other directions? Do we have (1) -> (2) or
>>>> (2) -> (3)? Can we construct models separating any/all of these three
>>>> statements?
>>>>
>>>> Thanks,
>>>> Ian
>>>>
>>>> --
>>>> 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.
>>
>> --
>> 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.

Re: [HoTT] Weaker forms of univalence

[Matt Oliveri]

[-- Attachment #1.1: Type: text/plain, Size: 2778 bytes --]

Why wouldn't a skeletal LCCC be a model of (1) + UIP?

On Thursday, July 20, 2017 at 1:57:37 PM UTC-4, Michael Shulman wrote:
>
> But is it known that this is definitely weaker?  E.g. are there models 
> that satisfy invariance but not the computation rule? 
>
> On Thu, Jul 20, 2017 at 4:59 AM, Steve Awodey <awo...@cmu.edu 
> <javascript:>> wrote: 
> > I think we’ve been through this before: 
> > 
> >  (1)  (A ≃ B) -> (A = B) 
> > 
> > is logically equivalent to what may be called “invariance”: 
> > 
> >         if P(X) is any type depending on a type variable X, then given 
> any equivalence e : A ≃ B , we have P(A) ≃ P(B). 
> > 
> > if we add to this a certain “computation rule”, we get something 
> logically equivalent to UA: 
> > assume p : A ≃ B → A = B; then given e : A ≃ B, we have p(e) : A = B is 
> a path in U. 
> > Since we can transport along this path in any family of types over U, 
> and transport is always an equivalence, 
> > there is a transport p(e)∗ : A ≃ B in the identity family. 
> > The required “computation rule” states that p(e)∗ = e. 
> > 
> > Steve 
> > 
> > 
> > 
> >> On Jul 20, 2017, at 8:56 AM, Bas Spitters <b.a.w...@gmail.com 
> <javascript:>> wrote: 
> >> 
> >>> It was observed previously on this list, 
> >> Maybe we should be using our wiki more? 
> >> https://ncatlab.org/homotopytypetheory/ 
> >> 
> >> 
> >> On Wed, Jul 19, 2017 at 7:19 PM, Michael Shulman <shu...@sandiego.edu 
> <javascript:>> wrote: 
> >>> It was observed previously on this list, I think, that full univalence 
> >>> (3) is equivalent to 
> >>> 
> >>> (4)  forall A, IsContr( Sigma(B:U) (A ≃ B) ). 
> >>> 
> >>> This follows from the fact that a fiberwise map is a fiberwise 
> >>> equivalence as soon as it induces an equivalence on total spaces, and 
> >>> the fact that based path spaces are contractible.  But the 
> >>> contractibility of based path spaces also gives (2) -> (4), and hence 
> >>> (2) -> (3). 
> >>> 
> >>> I am not sure about (1).  It might be an open question even in the 
> >>> case when A and B are propositions. 
> >>> 
> >>> 
> >>> On Wed, Jul 19, 2017 at 9:26 AM, Ian Orton <ri...@cam.ac.uk 
> <javascript:>> wrote: 
> >>>> Consider the following three statements, for all types A and B: 
> >>>> 
> >>>>  (1)  (A ≃ B) -> (A = B) 
> >>>>  (2)  (A ≃ B) ≃ (A = B) 
> >>>>  (3)  isEquiv idtoeqv 
> >>>> 
> >>>> (3) is the full univalence axiom and we have implications (3) -> (2) 
> -> (1), 
> >>>> but can we say anything about the other directions? Do we have (1) -> 
> (2) or 
> >>>> (2) -> (3)? Can we construct models separating any/all of these three 
> >>>> statements? 
> >>>> 
> >>>> Thanks, 
> >>>> Ian
>

[-- Attachment #1.2: Type: text/html, Size: 4675 bytes --]

Re: [HoTT] Weaker forms of univalence

[Peter LeFanu Lumsdaine]

[-- Attachment #1: Type: text/plain, Size: 3680 bytes --]

On Fri, Jul 21, 2017 at 2:36 AM, Matt Oliveri <atm...@gmail.com> wrote:

> Why wouldn't a skeletal LCCC be a model of (1) + UIP?
>

Because (1) would require not just the category itself to be skeletal, but
also its slices, if “(A ≃ B) -> (A = B)” is taken as a global axiom scheme, and
unlike for skeletality of the category itself, one cannot generally replace
a category by an equivalent one with suitably skeletal slices.

(If it’s taken as a quantified axiom “forall A,B:U, (A ≃ B) -> (A = B)”, as
it more usually is, then its validity doesn’t follow directly from any
amount of skeletality at all, but is to do with the specific universe
chosen.)

–p.



>
> On Thursday, July 20, 2017 at 1:57:37 PM UTC-4, Michael Shulman wrote:
>>
>> But is it known that this is definitely weaker?  E.g. are there models
>> that satisfy invariance but not the computation rule?
>>
>> On Thu, Jul 20, 2017 at 4:59 AM, Steve Awodey <awo...@cmu.edu> wrote:
>> > I think we’ve been through this before:
>> >
>> >  (1)  (A ≃ B) -> (A = B)
>> >
>> > is logically equivalent to what may be called “invariance”:
>> >
>> >         if P(X) is any type depending on a type variable X, then given
>> any equivalence e : A ≃ B , we have P(A) ≃ P(B).
>> >
>> > if we add to this a certain “computation rule”, we get something
>> logically equivalent to UA:
>> > assume p : A ≃ B → A = B; then given e : A ≃ B, we have p(e) : A = B is
>> a path in U.
>> > Since we can transport along this path in any family of types over U,
>> and transport is always an equivalence,
>> > there is a transport p(e)∗ : A ≃ B in the identity family.
>> > The required “computation rule” states that p(e)∗ = e.
>> >
>> > Steve
>> >
>> >
>> >
>> >> On Jul 20, 2017, at 8:56 AM, Bas Spitters <b.a.w...@gmail.com>
>> wrote:
>> >>
>> >>> It was observed previously on this list,
>> >> Maybe we should be using our wiki more?
>> >> https://ncatlab.org/homotopytypetheory/
>> >>
>> >>
>> >> On Wed, Jul 19, 2017 at 7:19 PM, Michael Shulman <shu...@sandiego.edu>
>> wrote:
>> >>> It was observed previously on this list, I think, that full
>> univalence
>> >>> (3) is equivalent to
>> >>>
>> >>> (4)  forall A, IsContr( Sigma(B:U) (A ≃ B) ).
>> >>>
>> >>> This follows from the fact that a fiberwise map is a fiberwise
>> >>> equivalence as soon as it induces an equivalence on total spaces, and
>> >>> the fact that based path spaces are contractible.  But the
>> >>> contractibility of based path spaces also gives (2) -> (4), and hence
>> >>> (2) -> (3).
>> >>>
>> >>> I am not sure about (1).  It might be an open question even in the
>> >>> case when A and B are propositions.
>> >>>
>> >>>
>> >>> On Wed, Jul 19, 2017 at 9:26 AM, Ian Orton <ri...@cam.ac.uk> wrote:
>> >>>> Consider the following three statements, for all types A and B:
>> >>>>
>> >>>>  (1)  (A ≃ B) -> (A = B)
>> >>>>  (2)  (A ≃ B) ≃ (A = B)
>> >>>>  (3)  isEquiv idtoeqv
>> >>>>
>> >>>> (3) is the full univalence axiom and we have implications (3) -> (2)
>> -> (1),
>> >>>> but can we say anything about the other directions? Do we have (1)
>> -> (2) or
>> >>>> (2) -> (3)? Can we construct models separating any/all of these
>> three
>> >>>> statements?
>> >>>>
>> >>>> Thanks,
>> >>>> Ian
>>
> --
> 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: 5917 bytes --]

Re: [HoTT] Weaker forms of univalence

[Jason Gross]

[-- Attachment #1: Type: text/plain, Size: 1133 bytes --]

Certainly (2) => (3), at least if you assume function extensionality; it
suffices to show that (\Sigma B, A ≃ B) is contractable, and since
contractibility and sigma respect equivalence, we can transfer the proof
that (\Sigma B, A = B) is contractable. I think the same is not true of
(1), though I'm not sure.

On Wed, Jul 19, 2017, 7:26 PM Ian Orton <ri...@cam.ac.uk> wrote:

> Consider the following three statements, for all types A and B:
>
>    (1)  (A ≃ B) -> (A = B)
>    (2)  (A ≃ B) ≃ (A = B)
>    (3)  isEquiv idtoeqv
>
> (3) is the full univalence axiom and we have implications (3) -> (2) ->
> (1), but can we say anything about the other directions? Do we have (1)
> -> (2) or (2) -> (3)? Can we construct models separating any/all of
> these three statements?
>
> Thanks,
> Ian
>
> --
> 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: 1605 bytes --]

Re: [HoTT] Weaker forms of univalence

[Michael Shulman]

I don't think you need function extensionality for contractibility and
Sigma to respect equivalence.  We need funext for Pi to respect
equivalence, but there are no Pis here.

On Wed, Jul 19, 2017 at 10:21 AM, Jason Gross <jason...@gmail.com> wrote:
> Certainly (2) => (3), at least if you assume function extensionality; it
> suffices to show that (\Sigma B, A ≃ B) is contractable, and since
> contractibility and sigma respect equivalence, we can transfer the proof
> that (\Sigma B, A = B) is contractable. I think the same is not true of (1),
> though I'm not sure.
>
> On Wed, Jul 19, 2017, 7:26 PM Ian Orton <ri...@cam.ac.uk> wrote:
>>
>> Consider the following three statements, for all types A and B:
>>
>>    (1)  (A ≃ B) -> (A = B)
>>    (2)  (A ≃ B) ≃ (A = B)
>>    (3)  isEquiv idtoeqv
>>
>> (3) is the full univalence axiom and we have implications (3) -> (2) ->
>> (1), but can we say anything about the other directions? Do we have (1)
>> -> (2) or (2) -> (3)? Can we construct models separating any/all of
>> these three statements?
>>
>> Thanks,
>> Ian
>>
>> --
>> 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.

Re: [HoTT] Weaker forms of univalence

[Jason Gross]

[-- Attachment #1: Type: text/plain, Size: 2502 bytes --]

> I am not sure about (1).  It might be an open > question even in the
> case when A and B are propositions.

If A and B are hProps, then (1) => (3) under function extensionality (not
sure if you can do away with out here).  The key idea is that there can be
only one equivalence between hProps. To prove contractibility, we must show
that (A, idequiv) = (B, e) for any equivalence e of A and B.  Let us prove
A = B by (1); what remains is proving that idequiv = transport (1) e.  It
now suffices to show that A ≃ A is an hProp for A an hProp.  This follows
from function extensionality.

On Wed, Jul 19, 2017, 8:28 PM Michael Shulman <shu...@sandiego.edu> wrote:

> I don't think you need function extensionality for contractibility and
> Sigma to respect equivalence.  We need funext for Pi to respect
> equivalence, but there are no Pis here.
>
> On Wed, Jul 19, 2017 at 10:21 AM, Jason Gross <jason...@gmail.com>
> wrote:
> > Certainly (2) => (3), at least if you assume function extensionality; it
> > suffices to show that (\Sigma B, A ≃ B) is contractable, and since
> > contractibility and sigma respect equivalence, we can transfer the proof
> > that (\Sigma B, A = B) is contractable. I think the same is not true of
> (1),
> > though I'm not sure.
> >
> > On Wed, Jul 19, 2017, 7:26 PM Ian Orton <ri...@cam.ac.uk> wrote:
> >>
> >> Consider the following three statements, for all types A and B:
> >>
> >>    (1)  (A ≃ B) -> (A = B)
> >>    (2)  (A ≃ B) ≃ (A = B)
> >>    (3)  isEquiv idtoeqv
> >>
> >> (3) is the full univalence axiom and we have implications (3) -> (2) ->
> >> (1), but can we say anything about the other directions? Do we have (1)
> >> -> (2) or (2) -> (3)? Can we construct models separating any/all of
> >> these three statements?
> >>
> >> Thanks,
> >> Ian
> >>
> >> --
> >> 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: 3490 bytes --]