ncfavier

open import Relation.Binary.PropositionalEquality
open ≡-Reasoning
open import Function.Base
open import Data.Empty
open import Data.Nat
open import Data.Nat.Properties
open import Data.Sum

data Bin : Set where
  ⟨⟩ : Bin

ncfavier

Require Import Arith ZArith Lia List Ascii String Program.Basics.
Open Scope string_scope.
Open Scope program_scope.
Import ListNotations.

(** The head character of a string, returned as a new string.
   If the string is empty, returns the empty string. *)

Definition head s := match s with
  | "" => ""

ncfavier

open import 1Lab.Path
open import 1Lab.Path.Groupoid
open import 1Lab.Type
open import 1Lab.Equiv

data Susp {ℓ} (A : Type ℓ) : Type ℓ where
  N S   : Susp A
  merid : A → N ≡ S

data Join {ℓ₁ ℓ₂} (A : Type ℓ₁) (B : Type ℓ₂) : Type (ℓ₁ ⊔ ℓ₂) where

ncfavier

open import 1Lab.Type
open import 1Lab.Path
open import 1Lab.Path.Groupoid
open import Data.Bool

data Niltok : Type where
  t : Niltok
  nicht : Niltok → Niltok
  mod2 : (n : Niltok) → n ≡ nicht (nicht n)
  coh : (n : Niltok) → ap nicht (mod2 n) ≡ mod2 (nicht n)

ncfavier

{-# OPTIONS --cubical #-}
module _ where

open import Cubical.Foundations.Everything
open import Cubical.Data.Nat
open import Cubical.Data.Sum
open import Cubical.Data.Empty as ⊥
open import Cubical.Relation.Nullary

data ℤ : Type where

ncfavier

{ size ? 1000 }: with builtins;
let
  enumerate = genList (i: i + 1);
  sum = foldl' add 0;
  divides = n: k: n / k * k == n;
  factors = n: filter (divides n) (enumerate (n / 2));
  perfect = n: sum (factors n) == n;
in
filter perfect (enumerate size)

ncfavier

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

open import Agda.Primitive

private variable
  ℓ ℓ' : Level
  A B : Set ℓ

data _≡_ {A : Set ℓ} : A → A → Set ℓ where
  refl : {a : A} → a ≡ a

ncfavier

{-# LANGUAGE MagicHash, UnboxedTuples #-}
import GHC.Prim
import Unsafe.Coerce
import Prelude hiding (id)

main :: IO ()
main = do
  print (id True)
  print (id False)
  print (id 15)

ncfavier

{-# LANGUAGE UnicodeSyntax #-}

-- n-ary functions s^n → a.
-- N s is the free Applicative on Reader s.
-- It encodes the effect "ask for one s", but since it's an Applicative
-- and not a Monad you can statically know how many arguments a function requires.
data N s a = Pure a | Ask (N s (s → a))

arity :: N s a → Integer
arity (Pure _) = 0

ncfavier

module LEM where

open import 1Lab.Type
open import 1Lab.Path
open import 1Lab.HLevel
open import 1Lab.HIT.Truncation
open import Data.Sum

⊥-is-prop : is-prop ⊥
⊥-is-prop ()