AndrasKovacs

{-# OPTIONS --without-K #-}

open import Data.Bool
open import Data.Product
open import Relation.Binary.PropositionalEquality
open import Data.Empty
open import Function

surj : {A B : Set} → (A → B) → Set
surj f = ∀ b → ∃ λ a → f a ≡ b

AndrasKovacs

{-# 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
open import Relation.Binary.PropositionalEquality public using (_≡_; refl; trans; subst; cong)

AndrasKovacs

{-# language Strict, LambdaCase, BlockArguments #-}
{-# options_ghc -Wincomplete-patterns #-}

{-
Minimal demo of "glued" evaluation in the style of Olle Fredriksson:

  https://github.com/ollef/sixty

The main idea is that during elaboration, we need different evaluation

AndrasKovacs

{-# language Strict, BangPatterns #-}

data Tm = Var Int | App Tm Tm | Lam Tm | Fix Tm deriving (Show, Eq)
data Val = VVar Int | VApp Val Val | VLam [Val] Tm | VFix [Val] Tm

isCanonical :: Val -> Bool
isCanonical VLam{} = True
isCanonical _      = False

eval :: [Val] -> Tm -> Val

AndrasKovacs

open import Data.Unit
open import Data.Product

infixr 4 _⇒_ _*_ ⟨_,_⟩ _∘_

data Obj : Set where
  ∙    : Obj
  base : Obj
  _*_  : Obj → Obj → Obj

AndrasKovacs

{-# language Strict, TypeApplications, ScopedTypeVariables,
    PartialTypeSignatures, ViewPatterns #-}
{-# options_ghc -Wno-partial-type-signatures #-}

import qualified Data.Primitive.PrimArray as A
import GHC.Exts (IsList(..))
import Data.Bits
import Data.Word
import Control.Monad.ST.Strict

AndrasKovacs

{-# language Strict #-}

import qualified Data.Primitive.PrimArray as A
import GHC.Exts (IsList(..))
import Data.Bits
import Data.Word

type Rule = A.PrimArray Word8

mkRule :: Word8 -> Rule

AndrasKovacs

{-# OPTIONS --postfix-projections --without-K --safe #-}

{-
Large countable ordinals in Agda. For examples, see the bottom of this file.
Checked with Agda 2.6.0.1.

Countable ordinals are useful in "big number" contests, because they
can be directly converted into fast-growing ℕ → ℕ functions via the
fast-growing hierarchy:

AndrasKovacs

{-# OPTIONS --without-K #-}

{-
Claim: finitary inductive types are constructible from Π,Σ,Uᵢ,_≡_ and ℕ, without
quotients. Sketch in two parts.

1. First, construction of finitary inductive types from Π, Σ, Uᵢ, _≡_ and binary trees.
   Here I only show this for really simple, single-sorted closed inductive types,
   but it should work for indexed inductive types as well.

AndrasKovacs

{-
Inductive-recursive universes, indexed by levels which are below an arbitrary type-theoretic ordinal number (see HoTT book 10.3). This includes all kinds of transfinite levels as well.

Checked with: Agda 2.6.1, stdlib 1.3

My original motivation was to give inductive-recursive (or equivalently: large inductive)
semantics to to Jon Sterling's cumulative algebraic TT paper: