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.

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