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.

ncfavier

{-# OPTIONS --no-import-sorts --erasure #-}
open import Agda.Primitive renaming (Set to Type)
open import Data.Nat
open import Data.Bool
open import Data.Product
open import Relation.Binary.PropositionalEquality

-- An element of `Remember a` is a witness that `a` exists at runtime.
data Remember {ℓ} {@0 A : Type ℓ} : (@0 a : A) → Type ℓ where
  instance remember : {a : A} → Remember a

ncfavier

module TerminalLarge where
open import 1Lab.Prelude

module
  _
  {ℓ}
  (X : Type ℓ)
  (Y : Type) (f : Y → X)
  (f-term : (Z : Type) (g : Z → X) → is-contr (Σ[ h ∈ (Z → Y) ] f ∘ h ≡ g))
  where

ncfavier

{-# OPTIONS --allow-unsolved-metas #-}
open import 1Lab.Prelude hiding (_∈_; el!)

module ResizingLoop where

module _ (all-prop : ∀ {ℓ} {A : Type ℓ} → is-prop A) where

  el! : Type → Ω
  el! A = el A all-prop

ncfavier

background

• constructive HoTT with propositional resizing and HIITs
• Ω := type of propositions = free DCPPO on 1
• Σ := Rosolini "dominance" (not constructively) / type of semidecidable propositions = conatural numbers quotiented by bisimilarity = (P : Ω) × ∃[ f : ℕ → 2 ] P = (∃[ i : ℕ ] f i = 0)
• Sσ := Sierpiński set = initial σ-frame (higher inductive type [1])
• S∨ := free countably-complete join-semilattice on 1 (higher inductive type [1])
• Sω := free ω-CPPO on 1 (higher inductive-inductive type [2])
• 2 := booleans
• any dominance P induces a mnd-container, hence a monad on sets which I call P-partiality

ncfavier

module bug where
open import Agda.Builtin.Equality
open import Data.Bool

module Acc
  (Level : Set)
  (_<_ : Level → Level → Set) where

  -- This definition somehow results in the arguments to U< being marked Nonvariant
  record Acc (k : Level) : Set where