[Agda] question about a form of irrelevance elimination

[Andreas Abel]

Agda's irrelevant quantification was inspired by Pfenning, LICS 2001, 
[1], and fleshed out for MLTT in Abel/Scherer, TYPES 2010.  The 
semantics provided there is via a term model, I am afraid.  In a PER 
model,  .A -> B  is just  Squash A -> B  where  (a1,a2) in Squash A iff 
there are a1' and a2' such that (a1,a2'), (a1',a2) in A.

Cheers,
Andreas

Reference [1]

@STRING{ieee	= "IEEE Computer Society Press" }
@STRING{lics01	= "16th IEEE Symposium on Logic in Computer Science (LICS
		  2001), 16-19 June 2001, Boston University, USA,
		  Proceedings" }

@InProceedings{	  pfenning:intextirr,
   author	= {Frank Pfenning},
   title		= {Intensionality, Extensionality, and Proof Irrelevance in
		  Modal Type Theory},
   booktitle	= lics01,
   publisher	= ieee,
   year		= 2001
}

Reference [2]

@STRING{lmcs	= "Logical Methods in Computer Science" }

@Article{	  abelscherer:types10,
   author	= {Andreas Abel and Gabriel Scherer},
   title		= {On Irrelevance and Algorithmic Equality in Predicative
		  Type Theory},
   journal	= lmcs,
   volume	= 8,
   number	= {1:29},
   year		= 2012,
   pages		= {1--36},
   note		= {TYPES'10 special issue.},
   ee		= {http://dx.doi.org/10.2168/LMCS-8(1:29)2012},
   bibsource	= {DBLP, http://dblp.uni-trier.de}
}

On 15.07.2015 22:51, Andrew Pitts wrote:
> On 15 July 2015 at 21:38, Peter LeFanu Lumsdaine
> <p.l.lumsdaine at gmail.com> wrote:
>> I think this sort of truncation should be consistent, at least with
>> Martin-Löf type theory (…I can’t speak to the rest of Agda’s type system…
>> ^_^ ) since it holds in the simplicial model, if I’m not mistaken.
>>
>> Precisely: given any fibration of simplicial sets, the inclusion of its
>> image (in the old-fashioned 1-categorical sense) is also a fibration; and
>> since it’s a monomorphism, any two sections of it are (judgementally) equal.
>> Moreover, all this is pseudo-stable under pullback in the base (i.e. stable
>> up to iso), so lifts to strictly stable structure in any of the standard
>> strictifications, and hence models this type theory.
>>
>> In SSets, this also admits an elimination principle, with a “propositional
>> computation rule”; this is not pseudo-stable, so will not (afaik) lift to
>> the Hofmann (right adjoint) strictification, but should lift to the
>> universes and local universes strictifications; so this should show that
>> this elimination principle for this “judgemental truncation” is also
>> consistent.
>
> Is there a reference for a semantics for the kind of irrelevance
> annotations that Agda provides, do you know?
>
> Andy
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>


-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Department of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden

andreas.abel at gu.se
http://www2.tcs.ifi.lmu.de/~abel/