JakobBruenker

open import Agda.Builtin.Sigma
open import Agda.Builtin.Equality

lemma : ∀ {a b} {A : Set a} {B : A → Set b} {x x' : A} {p p' : B}
      → (x , p) ≡ (x' , p') → ((x ≡ x') , (p ≡ p'))
lemma = ?

{-
Checking Test (/home/user/agda/combinators/Test.agda).
/home/user/agda/combinators/Test.agda:4,64-65

JakobBruenker

module Combinators where

open import Agda.Builtin.Nat renaming (Nat to ℕ)
open import Agda.Primitive
open import Agda.Builtin.Bool
open import Agda.Builtin.Equality
open import Agda.Builtin.Sigma
  renaming (fst to proj₁; snd to proj₂)
    hiding (module Σ)
module Σ = Agda.Builtin.Sigma.Σ

JakobBruenker

module Minimal where

open import Agda.Builtin.Nat renaming (Nat to ℕ)
open import Agda.Primitive
open import Agda.Builtin.Bool
open import Agda.Builtin.Equality
open import Agda.Builtin.Sigma

infixr 2 _×_

JakobBruenker

import java.util.function.Function;

// This is only actually a proof of anything if you assume that null doesn't
// exist, and that all functions are pure and terminate
public class WeakDNE {
    // False has no values
    public static final class False {
        private final Absurd absurdFun;

        // Helper interface to encode rank 2 type

JakobBruenker

{-# LANGUAGE GADTs
           , KindSignatures
           , DataKinds
           , PolyKinds
           , TypeFamilies
           #-}

import GHC.TypeLits hiding (Nat)

-- | Store a dict saying that one symbol is smaller than another

JakobBruenker

{-# LANGUAGE DataKinds
           , ScopedTypeVariables
           , TypeApplications
           , TypeFamilies
           , PolyKinds
           , StandaloneKindSignatures
           #-}

module MaybeBug where

JakobBruenker

{-# LANGUAGE TypeFamilies, UndecidableInstances, KindSignatures, DataKinds, TypeOperators, GADTs, RankNTypes, PolyKinds #-}

import Data.Kind
import Data.Type.Equality

data Nat = Z | S Nat

data SNat :: Nat -> Type where
  SZ :: SNat Z
  SS :: SNat n -> SNat (S n)

JakobBruenker

{-# LANGUAGE GADTs, TypeFamilies, DataKinds, TypeOperators, StandaloneDeriving #-}

module Dependent where

data Nat = Z | S Nat

data Vec (n :: Nat) a where
  Nil :: Vec Z a
  Cons :: a -> Vec n a -> Vec (S n) a

JakobBruenker

{-# LANGUAGE NumDecimals, BlockArguments #-}

import System.Environment
import Data.List

f 0 = (length .) . filter
f 1 = count
f 2 = count' 
f 3 = count''

JakobBruenker

{-# LANGUAGE ScopedTypeVariables
           , ViewPatterns
           , LambdaCase
           , BlockArguments
           , StandaloneKindSignatures
           , GADTs
           , TypeOperators
           , ImportQualifiedPost
           , UndecidableInstances
           , DerivingVia