Hello,
Sorry for the disturbance I cause but I still can not get the pairglob
function right it seems. The definition I sent you a few days ago used
a case construction which is unneccesary in the presence of the selectors
(eliminators) globroot and globchild. So I wrote a new pairglob using
globroot and globchild instead in hope for more success, but nope I can
not get it right.
Is there somewhere I can read more about the rec operator (gadget)?
/LL
------------------------------------------------------------------------------
[Formalization of (n-)category theory based on globular sets.]
------------------------------------------------------------------------------
( n : Nat !
data (---------! where (------------! ; !-------------!
! Nat : * ) ! zero : Nat ) ! suc n : Nat )
------------------------------------------------------------------------------
( m, n : Nat ! ( m : Nat ! ( m, n : Nat ; p : GtEq m n
!
data !------------! where !---------------! ;
!----------------------------!
! GtEq m n ! ! gteqz m : ! ! gteqs m n p :
!
! : * ) ! GtEq m zero ) ! GtEq (suc m) (suc n)
)
------------------------------------------------------------------------------
( C : * ; p : Zero !
let !-------------------!
! zeroelim C p : C )
zeroelim C p <= case p
------------------------------------------------------------------------------
( A, B : * ! ( a : A ; b : B !
data !--------------! where !---------------------!
! Pair A B : * ) ! pair a b : Pair A B )
------------------------------------------------------------------------------
( A, B : * ; p : (Pair A B) !
let !----------------------------!
! fst p : A )
fst p <= case p
{ fst (pair a b) => a
}
------------------------------------------------------------------------------
( A, B : * ; p : Pair A B !
let !--------------------------!
! snd p : B )
snd p <= case p
{ snd (pair a b) => b
}
------------------------------------------------------------------------------
[A globular set (glob A f) is a tree of ordinary sets (types). It has a root
!
!selected by (globroot (glob A f))=A:* this is the set of objects (0-cells)
!
!in standard category theory terminology. For every pair of objects
!
!a,b:(globroot (glob A f)) we have a child globular set
!
!(globchild (glob A f) a b)=(f a b):Glob the root of this tree i.e.
!
!(globroot (globchild (glob A f) a b)) is the (Hom)set of arrows (1-cells).
!
!In a theory with a stratified universe *n we should have Glob:*1.
]
------------------------------------------------------------------------------
( A : * ; f : all a, b : A => Glob !
data (----------! where !-----------------------------------!
! Glob : * ) ! glob A f : Glob )
------------------------------------------------------------------------------
( G : Glob !
let !----------------!
! globroot G : * )
globroot G <= case G
{ globroot (glob A G) => A
}
------------------------------------------------------------------------------
( G : Glob ; a, b : (globroot G) !
let !---------------------------------!
! globchild G a b : Glob )
globchild G a b <= case G
{ globchild (glob A B) a b => (B a b)
}
------------------------------------------------------------------------------
( G, H : Glob !
let !---------------------!
! pairglob G H : Glob )
pairglob G H <= rec G
{ pairglob G H <= rec H
{ pairglob G H => (glob (Pair (globroot G) (globroot H)) !
!% (lam a, a' : (Pair (globroot G) (globroot H))!!
! !=> (pairglob (globchild G (fst a) (fst a'))!!!
! ! !% (globchild H (snd a) (snd a')) )))
}
}
------------------------------------------------------------------------------
[Example of a globular set]
------------------------------------------------------------------------------
let (----------------!
! GtEqCat : Glob )
GtEqCat => (glob Nat (lam a, b : Nat => !!
! ! (glob (GtEq a b) !!!
! ! !% (lam p, q : (GtEq a b) => !!!!
! ! ! ! (glob Zero (lam v, w : Zero => !!!!!!
! ! ! ! ! ! (zeroelim Glob v)))))))
------------------------------------------------------------------------------
[In order to define category theory we need existance of certain elements
!
!(e.g.identity arrows) to some level n. E.g. in order to define the usual
!
!composition comp:Obj(a,b)xObj(b,c)->Obj(a,c) operator we need Obj(a,c) to
be !
!inhabited whenever Obj(a,b) and Obj(b,c) are. The identity require Obj(a,a)
!
!to be inhabitet. This correspond to proposition (Idfun (suc zero) G) for a
!
!globular set G.
]
------------------------------------------------------------------------------
( n : Nat ; G, H : Glob !
data !------------------------!
! Globfun n G H : * )
( n : Nat !
! !
! G, H : Glob !
! !
! f : all a : (globroot G) => (globroot H) !
! !
! h : !
! all a, b : (globroot G) => !
! (Globfun n (globchild G a b)! !
! !% (globchild H (f a) (f b))) ! ( G, H : Glob !
where !------------------------------------------! ; !--------------------!
! globfuns n G H f h : Globfun (suc n) G H ) ! globfunz : !
! Globfun zero G H )
------------------------------------------------------------------------------
( n : Nat
!
!
!
! G : Glob
!
!
!
! a : (globroot G)
!
!
!
! p :
!
( n : Nat ! ! all b : (globroot G) =>
!
! ! ! (Idfun n !
!
! G : Glob ! ( G : Glob ! ! !% (globchild G b b))
!
data !-----------! where !----------------! ;
!---------------------------!
! Idfun n G ! ! idfunz : ! ! idfuns n G a p :
!
! : * ) ! Idfun zero G ) ! Idfun (suc n) G
)
------------------------------------------------------------------------------
( n : Nat !
! !
! G : Glob !
! !
! id : (all a : (globroot G) => ! !
! ! (Idfun n (globchild G a a))) !
! !
! comp : (all a, b, c : (globroot G) => ! !
! ! (Globfun n !! !
! ! !% (pairglob (globchild G a b)!!! !
! ! ! !% (globchild G b c) )!! !
( n : Nat ! ! ! !% (globchild G a c) )) !
data !-----------! where !---------------------------------------------!
! Cat n : * ) ! cat n G id comp : Cat n )
------------------------------------------------------------------------------
[ Problem: ^^^^^^^^^^^^^^]
------------------------------------------------------------------------------
From: Conor McBride <[EMAIL PROTECTED]>
Reply-To: epigram@durham.ac.uk
To: epigram@durham.ac.uk, [EMAIL PROTECTED]
Subject: Re: [Epigram] Why does not Epigram accept this?
Date: Fri, 21 Oct 2005 11:16:43 +0100
Hi
Lars Lindqvist wrote:
Hi,
I downloaded Epigram a few days ago and have done some experiments. I have
not read all documentation in detail I have to admit. Why does not Epigram
accept the data definition in the bottom of the following section (see
Problem: ^^^^ at the bottoom of the mail)?
I have checked through the entrails (Alt-Return does an ugly proof-state
dump in the Epigram-bin buffer) and it's quite a subtle thing, relating to
some underimplemented functionality. Epigram isn't rejecting your
definition, as it happens: it's just not yet ready to believe it, because
it hasn't completed the positivity check on the definition. There's a bit
of the term missing, even though from here
------------------------------------------------------------------------------
( n : Nat !
! !
! G : Glob !
! !
! id : (all a : (globroot G) => ! !
! ! (Idfun n (globchild G a a))) !
! !
! comp : (all a, b, c : (globroot G) => ! !
! ! (Globfun n !! !
! ! !% (pairglob (globchild G a b)!!! !
! ! ! !% (globchild G b c) )!! !
( n : Nat ! ! ! !% (globchild G a c) )) !
data !-----------! where !---------------------------------------------!
! Cat n : * ) ! cat n G id comp : Cat n )
------------------------------------------------------------------------------
that's hard to see. In fact, the trouble is that the definition of pairglob
still contains a hole. Epigram fears that this hole might get filled with
an illegal occurrence of Cat, so it sticks. (In fact, Epigram should really
check the scope of the hole and realise that there's no way Cat can ever
occur in the definition of pairglob, but I didn't build any such cunning
into the positivity check.) What's the hole in pairglob?
------------------------------------------------------------------------------
( G, H : Glob !
let !---------------------!
! pairglob G H : Glob )
pairglob G H <= case G
{ pairglob (glob A B) H <= case H
{ pairglob (glob A B) (glob A' B')
=> (glob (Pair A! (lam a, a' : (Pair A A') => !!
! !% A' ) ! (pairglob (B (fst a) (fst a'))!!!
! ! !% (B' (snd a) (snd a')) )))
}
}
------------------------------------------------------------------------------
You can't see it, and that's my fault. The recursive call should be brown,
but I hacked up recursion-spotting rather clumsily, I'm afraid. Epigram
can't see why your recursive call makes sense, so it leaves a placeholder
for it. Of course, your recursion is entirely structural, so you need
merely say so. Replace pairglob with
------------------------------------------------------------------------------
( G, H : Glob ! let
!---------------------! ! pairglob
G H : Glob )
pairglob G H <= rec G
{ pairglob G H <= case G
{ pairglob (glob A B) H <= case H
{ pairglob (glob A B) (glob A' B')
=> (glob (Pair A! (lam a, a' : (Pair A A') => !!
! !% A' ) ! (pairglob (B (fst a) (fst a'))!!!
! ! !% (B' (snd a) (snd a')) )))
} }
}
------------------------------------------------------------------------------
and you're in business!
The state of diagnostic information in this system leaves some room for
improvement. My apologies.
Looks like fun stuff...
All the best
Conor
