Hi Bas,
thank you - indeed this is a very interesting observation. This was
the proof I had in mind when I first claimed that the axiom of choice
is provable in OTT. However, I was deluded in believing that OTT/
predicative topoi exactly characterize the theory of the setoid
model. As you clearl
Hi Conor,
I'm not sure I understand what's going on here.
This happens if you don't type check your definitions. I got carried
away with my non-dependent simplification of the story.
Thank you for actually reading it.
Indeed, in the setoid model we can construct a function
f : A -> [
Hi Thorsten
I'm not sure I understand what's going on here.
Thorsten Altenkirch wrote:
Indeed, in the setoid model we can construct a function
f : A -> [B]
--
lift f : [A -> B]
if the setoid A is "trivial", i.e. has the identity as its equivalence
relation.
I ca
Hi Thorsten,
On Thursday 01 February 2007 08:55:30 Thorsten Altenkirch wrote:
> thank you - indeed this is a very interesting observation. This was
> the proof I had in mind when I first claimed that the axiom of choice
> is provable in OTT. However, I was deluded in believing that OTT/
> predicat
Hi Bas,
thank you - indeed this is a very interesting observation. This was
the proof I had in mind when I first claimed that the axiom of choice
is provable in OTT. However, I was deluded in believing that OTT/
predicative topoi exactly characterize the theory of the setoid
model. As you
Hi Thorsten and others,
On Tuesday 30 January 2007 21:22:53 [EMAIL PROTECTED] wrote:
> I do indeed think that Observational Type Theory with quotient types should
> be the language of a Predicative Topos. I don't see in the moment that the
> setoid model would introduce anything which isn't provab
Hi Bas & everybody else,
I do indeed think that Observational Type Theory with quotient types should
be the language of a Predicative Topos. I don't see in the moment that the
setoid model would introduce anything which isn't provable in the Type
Theory and at least in the moment I don't see h
Dear Thorsten, Robin,
Now that the discussion has turned to setoids and observational type theory, I
could not help myself from responding. (Thorsten and I had quite some
off-line discussion about this).
I generally agree with Thorsten's description of observational type theory as
internalizin
Hi Robin,
The paper says "Observational reasoning can be simulated in
Intensional
Type Theory by the use of setoids, i.e. types with an explicit
equivalence relation".
I'm not clear on what the differences are between OTT and simulating
observational reasoning with setoids in ITT. Clearly OTT
Thanks to all who replied.
I have another couple of questions, more fundamental this time.
The paper says "Observational reasoning can be simulated in Intensional
Type Theory by the use of setoids, i.e. types with an explicit
equivalence relation".
I'm not clear on what the differences are betwe
I'd like to ask what /incompatible types/ Q equates for OTT in
(λu:1.u[Q> u)( u)):1
|-> ( u))[Q> ( u))
I think this program is clear to me only for ITT.
--
( Q : S = T ; s : S !
let !--
Hi Robin
I was just about to reply when I noticed Thorsten had...
Robin Green wrote:
I've been reading "Towards Observational Type Theory". I'm new to type
theory, so I have not been able to understand big chunks of the paper;
hopefully as I read wider I'll understand more of it.
However, one
Hi Robin,
I just saw Thorsten answered your e-mail. I'd better finish what I
started though.
I'm not an expert on OTT, but here are a few thoughts.
The "real" rule for coercion is the one on page 3. It doesn't require
the types to be definitionally equal. Section 5 mainly speculates on
a
Hi Robin,
thank you for your comments. Indeed we are currently revising this
paper, hence your comments are especially welcome.
I've been reading "Towards Observational Type Theory". I'm new to type
theory, so I have not been able to understand big chunks of the paper;
hopefully as I read wi
14 matches
Mail list logo
