TOTBWF

description
Idempotent systems.

open import Cat.Diagram.Monad
open import Cat.Prelude

import Cat.Reasoning
import Cat.Functor.Reasoning

TOTBWF

A short, self-contained proof that List A has UIP if A has UIP

First, we enable the --without-K flag, which removes UIP as an axiom. We also import Agda.Primitive, which gives us access to the Level type, though this isn't strictly required. We also add a variable block so we don't need to constantly abstract over types and levels.

{-# OPTIONS --without-K --safe #-}
module ListHLevels where

TOTBWF

{-# OPTIONS --lossy-unification #-}
open import Cat.Prelude

open import Data.List
open import Data.List.Member
open import Data.Sum

open import Theories.Signature

TOTBWF

open import 1Lab.Prelude

open import Data.Bool
open import Data.Fin
open import Data.List
open import Data.Nat

module Data.Bool.CNF where

TOTBWF

#include <fcntl.h>
#include <immintrin.h>
#include <stdio.h>
#include <sys/mman.h>
#include <sys/stat.h>

uint32_t parse_4_digits(const __m128i input) {
  const __m128i char_0 = _mm_set1_epi8('0');

  // Normalize the '0' char to actually be 0x00.

TOTBWF

module 1Lab.Reflection.Duh where

open import 1Lab.Reflection
open import 1Lab.Prelude
open import Data.List
open import Data.Nat

private
  try-all : Term → Nat → Telescope → TC Term
  try-all goal _ [] = typeError $ strErr "Couldn't find anything!" ∷ []

TOTBWF

(** Core Types *)
module Syntax =
struct
  type t =
    | Local of int
    | Hole of string
    | Let of string * t * t
    | Lam of string * t
    | Ap of t * t
    | Pair of t * t

TOTBWF

module NbE where

data Term
    = Var Int
    -- ^ DeBruijin Indicies (count outwards)
    | Lam Term
    | App Term Term
    | Pair Term Term
    | Fst Term
    | Snd Term

TOTBWF

{-# LANGUAGE TypeApplications #-}
module TwitterProblem where

import Data.SBV

--------------------------------------------------------------------------------
-- Complex Numbers, constructed from Algebraic Reals

data AlgComplex a = AlgComplex { real :: a, imaginary :: a}

TOTBWF

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

open import Categories.Category.Core
open import Categories.Category.Cartesian

module Categories.Tactic.Cartesian.Solver {o ℓ e} {𝒞 : Category o ℓ e} (cartesian : Cartesian 𝒞) where

open import Level

open import Categories.Category.BinaryProducts