ma82

Keybase proof

I hereby claim:

• I am ma82 on github.
• I am macerbi (https://keybase.io/macerbi) on keybase.
• I have a public key ASACGYT1PDwXyEbNzonJ2UtG7e0RJqH7ds6ESHxNmEVJoAo

To claim this, I am signing this object:

ma82

FROM jupyter/all-spark-notebook

USER root

RUN \
	wget "http://central.maven.org/maven2/org/apache/hadoop/hadoop-aws/2.7.3/hadoop-aws-2.7.3.jar"; \
	wget "http://central.maven.org/maven2/com/amazonaws/aws-java-sdk/1.7.4/aws-java-sdk-1.7.4.jar"; \
	wget "http://central.maven.org/maven2/joda-time/joda-time/2.9.3/joda-time-2.9.3.jar"; \
	wget "http://central.maven.org/maven2/mysql/mysql-connector-java/5.1.35/mysql-connector-java-5.1.35.jar"; \
	wget "https://storage.googleapis.com/hadoop-lib/gcs/gcs-connector-latest-hadoop2.jar"; \

ma82

# Questions about an axiom for equality of pointed sigma types

In the Agda 2.4.2.4 code below I am allowing K-based pattern matching.

## Basics

We need some standard imports and definitions.

\begin{code}
open import Level renaming (zero to Z ; suc to S)

ma82

See https://lists.chalmers.se/pipermail/agda/2015/007774.html and
related messages.

I'm using Agda maint-2.4.2, commit 7b727e0.

\begin{code}
module SymIter where

open import Data.Unit
import Level as L

ma82

# Finite sets and dependent sums

\begin{code}
module FiniteSigma where

open import Data.Bool
open import Data.Empty
open import Data.Fin as Fin
open import Data.Nat as ℕ using (ℕ ; zero ; suc)
open import Data.Sum as ⊎ renaming (inj₁ to inl ; inj₂ to inr)

ma82

# For Vectron!

## Base definitions

### Imports

\begin{code}
open import Data.Empty
open import Data.Unit
open import Data.Fin

ma82

open import Data.Nat using (ℕ ; zero ; suc)
open import Data.Product using (Σ ; _×_ ; _,_ ; ,_)
  renaming (proj₁ to fst ; proj₂ to snd ; curry to cu ; uncurry to uc)
open import Function using (id ; _∘_ ; _$_)
open import Level as L using (_⊔_)
open import Induction
open import Induction.Lexicographic
open import Induction.Nat
open import Relation.Binary.PropositionalEquality as ≡
  renaming (refl to <> ; sym to !_ ; cong₂ to ap₂) hiding ([_])

ma82

\begin{code}
{-# OPTIONS --without-K #-}
module Escardo20141101 where
\end{code}

\begin{code}
module Preamble where

  open import Level public
    using    (Level ; _⊔_)

ma82

\begin{code}
module EqMuId where
\end{code}

Empty, unit and equality.

\begin{code}
⊥ = (X : Set) → X
⊤ = (X : Set) → X → X

ma82

# No surjections from ℕ to ℕ^ℕ

\begin{code}
{-# OPTIONS --without-K #-}
module NatVsNat^Nat where
\end{code}

Preliminaries.

\begin{code}