[Agda] --without-K

[Nils Anders Danielsson]

Hi,

I have implemented a new flag, --without-K. From the release notes:

* The flag --without-K makes pattern matching more restricted. If the
   flag is activated, then Agda only accepts certain case-splits: if
   the type of the variable to be split is D pars ixs, where D is a
   data (or record) type, pars stands for the parameters, and ixs the
   indices, then ixs has to consist of distinct variables, and these
   variables must not be free in pars.

   The intended use of --without-K is to enable experiments with a
   propositional equality without the K rule. Let us define propositional
   equality as follows:

     data _≡_ {A : Set} : A → A → Set where
       refl : ∀ x → x ≡ x

   Then the obvious implementation of the J rule is accepted:

     J : {A : Set} (P : {x y : A} → x ≡ y → Set) →
         (∀ x → P (refl x)) →
         ∀ {x y} (x≡y : x ≡ y) → P x≡y
     J P p (refl x) = p x

   The same applies to Christine Paulin-Mohring's version of the J rule:

     J′ : {A : Set} {x : A} (P : {y : A} → x ≡ y → Set) →
          P (refl x) →
          ∀ {y} (x≡y : x ≡ y) → P x≡y
     J′ P p (refl x) = p

   On the other hand, the obvious implementation of the K rule is not
   accepted:

     K : {A : Set} (P : {x : A} → x ≡ x → Set) →
         (∀ x → P (refl x)) →
         ∀ {x} (x≡x : x ≡ x) → P x≡x
     K P p (refl x) = p x

   However, we have /not/ proved that activation of --without-K ensures
   that the K rule cannot be proved in some other way.

I have used the new flag to play around with Voevodsky's homotopy levels
and weak equivalence:

   http://www.cse.chalmers.se/~nad/listings/equality/README.html
   http://www.cse.chalmers.se/~nad/repos/equality/

Our usual hosting site is down at the moment. As an interim measure I
have uploaded the Agda repository to the following URL:

   http://www.cse.chalmers.se/~nad/repos/Agda/

-- 
/NAD