bobatkey

{-# OPTIONS --postfix-projections #-}

module tuple where





------------------------------------------------------------------------------
--

bobatkey

module localdefs where

mutual
  data ty-ctx : Set where
    ε    : ty-ctx
    _,-_ : (Δ : ty-ctx) → defn Δ → ty-ctx

  data defn : ty-ctx → Set where
    synonym : ∀ {Δ} → ty Δ → defn Δ
    newtype : ∀ {Δ} → ty Δ → defn Δ

bobatkey

{-# OPTIONS --prop --rewriting --confluence-check #-}

module param-rewrites where

open import Agda.Builtin.Unit

------------------------------------------------------------------------------
-- Equality as a proposition
data _≡_ {a} {A : Set a} : A → A → Prop where
  refl : ∀{a} → a ≡ a

bobatkey

{-# OPTIONS --rewriting #-}

module cont-cwf where

open import Agda.Builtin.Sigma
open import Agda.Builtin.Unit
open import Agda.Builtin.Bool
open import Agda.Builtin.Nat
open import Data.Empty
import Relation.Binary.PropositionalEquality as Eq

bobatkey

Require Import List.
Require Import FunctionalExtensionality.
Require Import ZArith.
Require Import Zcompare.

(* c.f. https://twitter.com/Hillelogram/status/987432184217731073 *)

Set Implicit Arguments.

Lemma map_combine : forall A B C (f : A -> B) (g : A -> C) xs,

bobatkey

This is a type constructor

class FunctionType:
    def __init__(self, tyA, tyB):
        self.tyA = tyA
        self.tyB = tyB

    def __eq__(self, other):
 return self.tyA == other.tyA and self.tyB == other.tyB

bobatkey

(* This is a demonstration of the use of the SML module system to
   encode (Generalized Algebraic Datatypes) GADTs via Church
   encodings. The basic idea is to use the Church encoding of GADTs in
   System Fomega and translate the System Fomega type into the module
   system. As I demonstrate below, this allows things like the
   singleton type of booleans, and the equality type, to be
   represented.

   This was inspired by Jon Sterling's blog post about encoding proofs
   in the SML module system: