Downcasing LCCCs

(You are not expected to understand this!)

• 1. Rules (from Jacobs's book)
• 2. Strong sums and strong equality
• 3. Shorthands for LCCC notation

1. Rules (from Jacobs's book)
=============================
From Sec. 10.1, pp.584-594.

Projection:     a|-B
               ------
               a,b|-b

Substitution:  a|-b   a,b,c|-D/d
               -----------------
                   a,c|-D/d

Contraction:   a,b,b',c|-D/d
               -------------
                a,b,c|-D/d

Weakening:     a|-B   a|-C/c
               -------------
                 a,b|-C/c

Exchange:      a,b,c,d|-E/e
               ------------
               a,c,b,d|-E/e

Unit type:               a|-*'
            ---   ---   -------
            |-1   |-*   a|-*=*'

Π, Σ, Eq:   a,b|-C     a,b|-C         a|-B	      
	    -------    -------    ---------------
  	    a|-Πb.C    a|-Σb.C    a,b,b'|-W[b=b']

	    a,b|-c     a|-b   a|-b|->c
	   --------    ---------------
	   a|-b|->c        a|-c

	  a,b|-C       a|-D   a,b,c|-d
       ------------    ---------------(weak)
       a,b,c|-<b,c>      a,(b,c)|-d

	    a|-B       a,b,b',c|-D   a,b,\barc|-\bard
	 ----------    ------------------------------(weak)
	 a,b|-(b=b)         a,b,b'(b=b'),c|-d

Page: 588: some conversions.
I haven't typed them yet...

2. Strong sums and strong equality
==================================

  a,(b,c)|-D   a,b,c|-d
  ---------------------(strong)
      a,(b,c)|-d

  a,b,b',(b=b')|-C   a,b|-\barc
  -----------------------------(strong)
       a,b,b'(b=b')|-c
  
Proposition (10.1.3, p.589):
these strong elimination rules
can be equivalently formulated as:

  a|-(b,c)    a|-(b,c)
  --------    --------
    a|-b        a|-c

  a|-(b=b')      a|-(b=b')
  ---------   ---------------(???)
   a|-b=b'    a|-(b=b')=(b=b)

3. Shorthands for LCCC notation
===============================
(From Seely's paper)

Some term formation rules:

    a|-b
  --------(=I)      Shorthand:
  a|-(b=b)          (b=b) := r(b)

     a,b|-d
  --------------(=E)
  a,b,b',e|-σ(d)


Some equality rules:

     a,b|-d
  --------------
  a,b,b',e|-σ(d)
  --------------  (= red)
    a,b|-σ(d)        =    a,b|-d

  a,b,b',e|-f
  -----------
     a,b|-f
  -----------     (= exp)
  a,b,b',e|-σ(f)     =    a,b,b',e|-f


  a|-b  a|-b'  a|-e
  -----------------(Irule1)
      a|-b=b'
  
  a|-b  a|-b'  a|-e
  -----------------(Irule2)
      a|-e=(b=b')