rzrn

universe u

inductive Eq' {A : Type u} : A → A → Type u
| idp (a : A) : Eq' a a

def f {A : Type u} {a b : A} : Eq' a b → Eq a b :=
λ q => @Eq'.casesOn A a (λ b q' => Eq a b) b q (Eq.refl a)

def g {A : Type u} {a b : A} : Eq a b → Eq' a b :=
λ p => @Eq.casesOn A a (λ b p' => Eq' a b) b p (Eq'.idp a)

rzrn

#! /usr/bin/bash

# $ echo -n Π U Z Π 0 Π 1 U Z > Id
# $ ./dtt.sh λ U Z λ 0 λ 1 β β β Id 2 1 0
# INFER: Π U Z Π 0 Π 1 U Z
# EVAL: λ U Z λ 0 λ 1 β β β Id 2 1 0

function head() {
    echo $* | cut -d" " -f1
}

rzrn

import Lean.Elab.Command
open Lean

elab "#defeq " σ₁:term " =?= " σ₂:term : command =>
  Elab.Command.liftTermElabM (do
    let τ₁ ← Elab.Term.elabTerm σ₁ none
    let τ₂ ← Elab.Term.elabTerm σ₂ none
    unless (← Meta.isDefEq τ₁ τ₂) do throwError s!"{τ₁} ≠ {τ₂}")

#defeq [1, 2, 3, 4].reverse =?= [4, 3, 2, 1]

rzrn

noncomputable section
namespace MWE

universe u v w

inductive Id {A : Type u} : A → A → Type u
| refl {a : A} : Id a a

attribute [eliminator] Id.casesOn

rzrn

module patt where

data nat
  = zero
  | succ (n : nat)

natToZero : nat -> nat = split
  zero ha ha ha -> zero
  succ cubicaltt is a w e s o m e -> zero

rzrn

import Lean.Meta.Reduce
import Lean.Parser.Term
import Lean.Expr
import Lean.Elab
open Lean

axiom I  : Type
axiom i₀ : I
axiom i₁ : I

rzrn

from dataclasses import dataclass
from random import random

@dataclass
class Vector:
    x : float
    y : float

    def __sub__(v1, v2):
        return Vector(v1.x - v2.x, v1.y - v2.y)

rzrn

module inv where

Path (A : U) (a b : A) : U = PathP (<_> A) a b

inv1 (A : U) (a b : A) (p : Path A a b) : Path A b a =
  <i> p @ -i

inv2 (A : U) (a b : A) (p : Path A a b) : Path A b a =
  <i> comp (<_> A) a [(i = 0) -> p, (i = 1) -> <_> a]

rzrn

type path =
  | Var of string
  | Ref
  | Trans of path * path
  | Rev of path

let rec show : path -> string = function
  | Var x -> x
  | Ref -> "ref"
  | Trans (p, q) -> Printf.sprintf "(%s * %s)" (show p) (show q)

rzrn

{-# OPTIONS --cubical #-}
module Experiments where

open import Agda.Builtin.Cubical.Path public
open import Agda.Builtin.Cubical.Sub public renaming (primSubOut to ouc)
open import Agda.Primitive.Cubical public
  renaming ( primIMin       to _∧_  -- I → I → I
           ; primIMax       to _∨_  -- I → I → I
           ; primINeg       to -_   -- I → I
           ; isOneEmpty     to empty