shlevy

namespace category
  universes u v

  structure category :=
    (object : Type u)
    (arrow : object → object → Type v)
    (identity : Π {α}, arrow α α)
    (compose : Π {α β φ}, arrow β φ → arrow α β → arrow α φ)
    (infixr ∘ := compose)
    (compose_left_identity_unit : ∀ α β (f : arrow α β), identity ∘ f = f)

shlevy

Keybase proof

I hereby claim:

• I am shlevy on github.
• I am shlevy (https://keybase.io/shlevy) on keybase.
• I have a public key whose fingerprint is 37DC 4CAB 574E D7A7 679A CC0B F483 E15E 3911 8520

To claim this, I am signing this object:

shlevy

#!/usr/bin/env bash

set -e

name=$(nix-instantiate "$@" -A name --eval | tr -d '\n"')

mkdir -p $HOME/.cache/envs

env=$HOME/.cache/envs/$name

shlevy

$ "inplace/bin/ghc-stage1" -keep-tmp-files -hisuf hi -osuf  o -hcsuf hc -static  -O0 -H64m -Wall      -this-unit-id base-4.9.0.0 -hide-all-packages -i -ilibraries/base/. -ilibraries/base/dist-install/build -ilibraries/base/dist-install/build/autogen -Ilibraries/base/dist-install/build -Ilibraries/base/dist-install/build/autogen -Ilibraries/base/include    -optP-include -optPlibraries/base/dist-install/build/autogen/cabal_macros.h -package-id ghc-prim-0.5.0.0 -package-id integer-simple-0.1.1.1 -package-id rts -this-unit-id base -XHaskell2010 -O -fllvm  -no-user-package-db -rtsopts -Wno-trustworthy-safe -Wno-deprecated-flags     -Wnoncanonical-monad-instances  -odir libraries/base/dist-install/build -hidir libraries/base/dist-install/build -stubdir libraries/base/dist-install/build    -c libraries/base/./GHC/Float.hs -o libraries/base/dist-install/build/GHC/Float.o
ld: warning: directory not found for option '-L/nix/store/2vd6b82fih97l9bd77ykyvr0b359ircg-clang-wrapper-3.7.1/lib'
ld: warning: directory not found

shlevy

var walker = document.createTreeWalker(document.body, NodeFilter.SHOW_TEXT);

while (walker.nextNode()) {
    var newText = walker.currentNode.nodeValue.replace(/(\d+\s*)?π/g, function (match, multiplierString) {
        var multiplier = parseInt(multiplierString.trim(), 10);
        if (isNaN(multiplier)) {
            return "τ/2";
        } else if (multiplier == 2) {
            return "τ";
        } else {

shlevy

running tests
Running 1 test suites...
Test suite regression-and-sanity-tests: RUNNING...
basic001 finished...FAILURE
0a1,2
> 1f4o1b4a1r1b3a1z
> 1f4o1b4a1r1b3a1z
basic002 finished...FAILURE
0a1,5
> test006.idr:25:23-28:

shlevy

%default total

codata Level : Type where
  S : Level -> Level

sInjective' : (x : Level) -> (y : Level) -> S (Delay x) = S (Delay (Force (Delay (S (Delay y))))) -> x = S (Delay (Force (Delay y)))
sInjective' _ y Refl = replace {P = \level => S (Delay y) = S (Delay level)} Refl Refl

levelNotSLevel' : (level : Lazy' LazyCodata Level) -> Not ((Force level) = S level)
levelNotSLevel' (S (Delay level)) p = levelNotSLevel' level (sInjective' level level p)

shlevy

conn inbound
  leftid=it-services@zalora.com
  type=transport
  auto=add
conn outbound-1
  leftid=it-services@zalora.com
  right=192.168.56.103
  rightid=it-services@zalora.com
  type=transport
  auto=route

shlevy

conn inbound
  leftid=it-services@zalora.com
  leftcert=/etc/x509/strongswan.crt
  type=transport
  auto=add

conn outbound
  leftid=it-services@zalora.com
  leftcert=/etc/x509/strongswan.crt
  right=192.168.56.101

shlevy

conn inbound
  left=%any
  right=%any
  rightid=%any
  auto=add
  type=transport
  leftcert=/etc/x509/strongswan.crt

conn outbound
  left=%any