[ admin ] backport to Agda 2.5.4.2 and stdlib 0.17

Looks like 2.6.0 and 1.0 won't be released in time for the talk.
So I'm rolling back the compatibility changes and sticking to the
stable releases.

Author: gallais

src/Generic/Identity.agda

@@ -17,7 +17,7 @@ open import Generic.Simulation.Syntactic
 
 open import Function
 open import Relation.Binary.PropositionalEquality as PEq
-open import Relation.Binary.PropositionalEquality.WithK
+-- open import Relation.Binary.PropositionalEquality.WithK
 open ≡-Reasoning
 
 -- If we directly try to prove that t[id] ≡ t we run into size-related issues.
@@ -54,7 +54,7 @@ module _ {I : Set} {d : Desc I} where
 
  ⟨ `σ A d   ⟩≅⇒≡ (refl , eq) = cong -,_ (⟨ d _ ⟩≅⇒≡ eq)
  ⟨ `X Δ j d ⟩≅⇒≡ (≅-pr , eq) = cong₂ _,_ (≅⇒≡ ≅-pr) (⟨ d ⟩≅⇒≡ eq)
- ⟨ `∎ i     ⟩≅⇒≡ eq          = ≡-irrelevant _ _
+ ⟨ `∎ i     ⟩≅⇒≡ eq          = ≡-irrelevance _ _
 
 -- We can now prove a lemma stating that t[id] ≅ t and we will obtain t[id] ≡ t as
 -- a corrolary.

travis/install_agda.sh

@@ -5,12 +5,17 @@ if ! type "agda" > /dev/null || [ ! `agda -V | sed "s/[^2]*//"` = "$AGDA_VERSION
   cabal update
   cabal install alex happy cpphs --force-reinstalls
   cabal install Agda-"$AGDA_VERSION" --force-reinstalls
+  mkdir -p $HOME/.agda
+  cp libraries-${VERSION} $HOME/.agda/
+  cd $HOME/.agda/
+  wget https://github.com/agda/agda-stdlib/archive/v0.17.tar.gz
+  tar -xvzf v0.17.tar.gz
+  cd -
 fi
 
-mkdir -p $HOME/.agda
-cp libraries-"$AGDA_VERSION" $HOME/.agda/
-cd $HOME/.agda/
-git clone https://github.com/agda/agda-stdlib/ agda-stdlib-0.18
-cd agda-stdlib-0.18
-git checkout a0bfe7422d2aa0f0f49c9647659ce34e6e741375
-cd -
+# mkdir -p $HOME/.agda
+# cp libraries-"$AGDA_VERSION" $HOME/.agda/
+# cd $HOME/.agda/
+# git clone https://github.com/agda/agda-stdlib/ agda-stdlib-0.18
+# cd agda-stdlib-0.18
+# git checkout a0bfe7422d2aa0f0f49c9647659ce34e6e741375

travis/libraries-2.5.4.2

@@ -1 +1 @@
-$HOME/.agda/agda-stdlib-0.18/standard-library.agda-lib
+$HOME/.agda/agda-stdlib-0.17/standard-library.agda-lib