ncfavier

{-# OPTIONS --safe --cubical-compatible --erasure --erased-quotients --no-import-sorts #-}
open import Agda.Primitive renaming (Set to Type)
open import Agda.Builtin.Equality
open import Agda.Builtin.Erased.Quotient

cong : ∀ {ℓa ℓb} {A : Type ℓa} {B : Type ℓb} {x y} (f : A → B) → x ≡ y → f x ≡ f y
cong f refl = refl

_∙_ : ∀ {ℓ} {A : Type ℓ} {x y z : A} → x ≡ y → y ≡ z → x ≡ z
refl ∙ p = p

ncfavier

module Canonicity where
open import 1Lab.Prelude
open import Data.Sum

-- let T = DTT[B : Ty, t f : Tm B]

-- higher-order T-algebras
record TAlg : Type₁ where
  no-eta-equality
  field

ncfavier

open import Agda.Builtin.Nat
open import Agda.Builtin.Equality

data ⊥ : Type where

module M (n : Nat) where
  -- Γ = (n : Nat)

  -- full type : (n : Nat) (a : ⊥) (m : Nat) → n ≡ m → ⊥
  foo : (a : ⊥) (m : Nat) → n ≡ m → ⊥

ncfavier

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.GroupoidLaws
open import Cubical.Foundations.Transport
open import Cubical.Foundations.Function
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Univalence

private variable
  ℓ : Level
  A : Type ℓ

ncfavier

open import Cubical.Algebra.Group.Free
open import Cubical.Data.Bool
open import Cubical.Data.Empty as ⊥
open import Cubical.Data.List renaming (elim to elimList)
open import Cubical.Data.Sum
open import Cubical.Foundations.Function
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Prelude
open import Cubical.HITs.FreeGroup
open import Cubical.HITs.FreeGroup.NormalForm

ncfavier

open import 1Lab.Prelude
open import 1Lab.Reflection
open import Order.Base

module eq-rel where

record is-equivalence-relation
  {ℓ} {A : Type ℓ} ℓ≈ (_≈_ : A → A → Type ℓ≈)
  : Type (ℓ ⊔ ℓ≈) where
  no-eta-equality

ncfavier

postulate
  X : Set
  u : X
  P : X → Set
  Q : P u → Set

f : (p : P u) → Q p
f p with u | p
... | a | b = ?
-- f.with : (p : P u) (w : X) (p' : P w) → Q p'

ncfavier

{-# OPTIONS --without-K #-}
module W where
open import Data.Container.Core
open import Data.Container.Relation.Unary.All
open import Data.W
open import Data.Product
open import Relation.Binary.PropositionalEquality

-- Originally asked by Jasper Hugunin at https://stackoverflow.com/questions/79894235

ncfavier

{-# OPTIONS --type-in-type --with-K #-}

open import Data.Product
open import Relation.Binary.PropositionalEquality
open import Relation.Nullary
open import Data.Empty

{-
Russell's paradox can be encoded in MLTT + K + U:U, as formalised in
https://github.com/KonjacSource/Russell-paradox-in-TT.

ncfavier

#!/usr/bin/env nix-shell
#!nix-shell --pure -i runghc -p "haskellPackages.ghcWithPackages (pkgs: with pkgs; [ graphviz topograph ])"
{-
A simple script that reads a dot graph from standard input, restricts
it to the *subposet* on the labels given as arguments (that is, computes
the transitive reduction of a subgraph of its transitive closure) and
prints the result to standard output.

Node and edge labels are destroyed, and the output graph uses input
labels as node IDs.