mac apps

Makefile

@@ -18,6 +18,8 @@ post-htmls   := $(patsubst $(src)/%.md,$(www)/%.html,$(post-sources))
 .PHONY: all serve clean $(POSTCC)
 
 all: $(POSTCC) $(post-htmls) $(post_index) $(feed) $(www_root)/static
+	@echo "\n"
+	@echo "Copying the ORG-produced files..."
 	cp -R ~/www/* $(www_root)
 
 $(www)/%.html: $(src)/%.md

content/leibniz-equality.md

@@ -0,0 +1,83 @@
+title: Leibniz equality for truncated types in HoTT
+tags: type theory
+date: 2021-01-19 00:00
+---
+
+Leibniz equality states that two things are equal if they are
+industinguishable by any predicates. For a type `A` and `a, b : A`:
+
+    Leq(A, a, b) ≡ ∏ (P : A → Prop), P a ⇔ P b
+
+In the language of HoTT we can restate the definition slightly:
+
+    Leq(A, a, b) ≡ ∏ (P : A → hProp), P a = P b
+
+where the last equality is equality of hProps: `P a =_hProp P b`.
+Since `hProp : hSet`, we have that `P a =_hProp P b : hProp` and,
+hence `Leq(A, a, b) : hProp`.
+
+Because `Leq` is a proposition it cannot describe fully the actual
+identity type `Id(A, a, b)`. But it does accurately desctibe the
+equality in hSets.
+
+Let `A : hSet`. Then we can define `Leq(A, a, b) <-> Id(A, a, b)`.
+First, we define `f : Id(A, a, b) → Leq(A, a, b)` by
+
+    f(p : a = b) ≡ λ (P : A → hProp). ap P p
+
+In the other direction we define `g : Leq(A, a, b) → Id(A, a, b)`.
+Suppose we have `H : Leq(A, a, b)`. Then we just pick `h(x) ≡ (a = x)`,
+and `H(h) : (a = a) = (a = b)`, which we apply to `1_a`.
+
+    g(H : ∏ P, P a = P b) ≡
+        let h = (λx. a = x) : A → hProp in
+        transport (λ X. X) (H(h)) (idpath a)
+
+So, for the equality on `hSet`s, the Leibniz equality coincides with
+the ML indentity type.
+
+The question that I have is whether we can generalize it and define a
+complete tower of Leibniz equalities?
+This is what I mean, specifically.
+
+For an (n+1)-Type `A` and `a, b : A`, we can define `Leq_n(A, a, b) :
+n-Type` as:
+
+    Leq_n(A, a, b) ≡ ∏ (P : A → n-Type), P a =_{n-Type} P b
+
+We can still reuse the same functions `f` and `g`, which type check
+correctly. We can also show:
+
+    g(f(p : a = b)) = p
+
+By induction
+   
+    g(f(1_a)) = g(λP. ap P 1_a) = g (λP. 1_{P_a}) =
+    (idpath (h(a) = h(a)))*(1_a) = 1_a
+
+So we have a section `a = b → Leq_n(A, a, b)`. But showing that `f(g(H))
+= H` is complicated. It would be nice to see if it can be derived
+somehow.
+
+In order to show that `f(g(H)) = H`, you need to show that for any `P`,
+
+    ap P (transport (H (λx. a = x)) 1a) = H P
+
+Note that all the elements in the image of `f` satisfy this condition.
+So perhaps it will make sense to restrict the type `Leq(A, a, b)` to
+contain only such `H`s that satisfy the condition above?
+I am not sure, but it is something that might be worth looking into.
+
+
+Note that the definition of Leibniz equality that we consider here is different from the "unrestricted" Leibniz equality:
+
+    Leq_Type(A, a, b) ≡ ∏ (P : A → Type), P a ↔ P b
+
+This Leibniz equality type has been studied in the context of intensional type theory in ["Leibniz equality is isomorphic to Martin-Löf identity, parametrically"](https://www.cambridge.org/core/journals/journal-of-functional-programming/article/abs/leibniz-equality-is-isomorphic-to-martinlof-identity-parametrically/50D76A9C314AB24E7CD46DA4A0A766EB) by Abel, Cockx, Devriese, Timany, and Wadler.
+They show that, under the assumptions of parametricity/under the parametricity translation, the above `Leq_Type` is isomorphic to the standard intensional equality type.
+
+It might be interesting to compare the "truncated" and "unrestricted" Leibniz equality types.
+For example, we can represent a type as a [colimit of a sequence of n-truncations](https://homotopytypetheory.org/2014/06/30/fibrations-with-em-fiber/).
+Does this connection somehow lift to representation of `Leq_Type` in terms of `Leq_n`'s?
+
+Let me know if you have any ideas on this topic.

content/mac-apps.md

@@ -0,0 +1,60 @@
+title: Useful Mac OS programs
+tags: macos, computers
+date: 2022-03-11 00:00
+---
+
+Somewhat recently I got a MacBook Pro for work. I already use other
+Apple products and I figured that being a UNIX based system it is
+going to be very much useable for work related things. And, of course,
+I was curious about their new M1 soc. At the end, I was a bit
+dissapointed with the user experience and the desktop environment,
+coming from Linux/X11.
+
+After some rudimentary research, I found the following programs to be
+very useful, and I highly recommend them for improving your
+interactions with the Mac OS. All of the programs below are free
+software and can be installed using Homebrew.
+
+For GUI/DE:
+- [Hammerspoon](http://www.hammerspoon.org/) for configuring keyboard
+  shortcuts for maximazing windows, snapping them around, etc. It is a
+  general-purpose "automation" tool, and it is scripted in Lua. You
+  can really do a lot of things with it, and I barely scratch the
+  surface with my [very modest configuration file](https://git.groupoid.moe/dan/dotfiles/src/branch/master/hammerspoon/.hammerspoon/init.lua).
+- [Easy Move+Resize](https://github.com/dmarcotte/easy-move-resize)
+  for moving and resizing windows like in Linux/X11 by using
+  Ctrl-Shift-right mouse and Ctrl-Shift-left mouse and dragging the
+  window. Super useful.
+- BackgroundMusic for per-app sound
+  control. I was really surprised this is not implemented by default
+  in Mac OS.
+- [Mos](https://mos.caldis.me/). A tool to fix the broken mouse
+  behavior on Mac OS. In Mac OS you can use two scrolling directions:
+  "natural scrolling" (which is great for touch pads) and the standard
+  scrolling (which is great for standard mices). Unfortunately, you
+  can only select one direction which applies to *all* of your
+  devices! So, you need to install Mos to implement the scrolling
+  properly.
+
+
+For LaTeX workflow:
+- Mitsuharu Yamamoto's [emacs-mac port](https://bitbucket.org/mituharu/emacs-mac/src/master/),
+  also available [via homebrew](https://github.com/railwaycat/homebrew-emacsmacport).
+  It beats the other Emacs ports for MacOS by integrating some
+  Mac-specific niceties like smooth scrolling, correctly registering
+  fullscreen, etc. You you install it from source, and you gcc and
+  libgccjit, you can enable native compilation for elsip.
+- [Skim](http://skim-app.sourceforge.net/) for PDF viewing. Works
+  flawlessly with Emacs/SyncTeX. Backwards search with
+  Shift-Command-click.
+
+Other useful utilities:
+- [Stats.app](https://github.com/exelban/stats) for monitoring
+  resource usage, fans, temperature, etc.
+- [IINA](https://iina.io/). Basically a frontend to `mpv`. Great media
+  player.
+- [iTerm2](https://iterm2.com/). Easy to use terminal emulator.
+- For unknown reason, stock MacOS does not support per-app volume
+  settings. Even as a frequent hater of the audio on Linux, I have to
+  admit that this just puzzled me. You need to donwload a separate
+  app, BackgroundMusic, and route all of your audio throught it.

drafts/switches.md

@@ -0,0 +1,136 @@
+title: Mechanical keyboard switchees
+tags: computers, keyboards
+date: 2022-04-24 00:00
+---
+
+I am trying something new. Here I will be recording my thoughts about
+various keyboard switches I tried.
+
+
+# Tactile
+
+**Gazzew Boba U4**
+
+Silent high-tactility switch, 65g. Does not produce a lot of sound, but not
+_completely_ quite. Great tactility with a sharp early bump. I tend to
+bottom out easily when typing on these.
+
+My favourite switch so far, in terms of pure tactility.
+
+**Gazzew Boba U4T**
+
+High-strength tactile switch. All bump, no pre/post-travel. Feels very
+nice. The sound is supposed to be "thocky", but I subjectively found
+it more "poppy" than SP Star Magic Girl, for example, which tends to
+have a more muted sound. Overall, a great switch with an amazing
+tactile signature and a moreish sharp bump.
+
+**Durock T1**
+
+TBD
+
+**Glorious Panda**
+
+I have not tried the original Holy Pandas yet, but I was told that
+Glorious Panda can be a sufficient replacement. So far I have been
+enjoying those switches. They are on the more heavy tactile end of
+things with a sharp bump (still not as heavy as Boba U4 dd, and not as
+sharp as Kailh Box Royal). The sound is alright, not too annoying, and
+it seems to improve with some lubing on the housing. However, under
+heavy typing there can be a noticable ping.
+
+**Purple Panda**
+
+Mid-high-strength tactil from Tecsee, 68g. Another take on the "Holy
+Panda" signature with a P-shaped bump. However, the stem is very long,
+resulting in very short travel (3mm?). Because of that, the
+post-travel is rather small, and it is not very hard to bottom out
+with these switches. The upstroke also feels very fast.
+
+Initially when I got them, there was very little ping stock. However,
+after using them actively for a week I think the ping has gotten
+worse.
+
+Comparison with some other tactile switches:
+
+- Compared to Glorious Panda, Purple Pandas have shorter post-travel and
+a more rounded bump. Purple Pandas also have less ping.
+
+- Tecsee Sapphire
+Techsee Sapphire have a much shorter, lighter bump, and have way more post-travel.
+
+
+- SP Star Magic Girl.
+The Magic Girl switches have a generally similar tactile signature,
+with almost no pre-travel before the bump. The bump on Magic Girl
+feels longer than on Purple Panda. Despite of that, the post-travel on
+Purple Panda is shorter than that on Magic Girl, probably due to the
+stem length.
+
+
+- Compared to SP Star Magic Girl, Purple Pandas have a way shorter ..
+
+**SP Star Magic Girl**
+
+Mid-to-high-strength colourful tactiles. A pronounced but rounded bump
+with very little pre-travel. Smooth for the post-bump travel. Since
+the post-travel is longer than on some other tactiles (probably the
+most post-bump travel on this list, at the time of writting), it is
+quite possible not to bottom out on every keypress. Sound-wise they
+are kind of muted. Not silent, but with quiter typing force the sounds
+of keycaps etc will easily drown on the switch-proper sounds. For
+example, compared to Box Royals or Glorious Pandas, these have way
+less ping.
+
+**Kailh Box Royal**
+
+Mid-strength tactile, on the more tactile end of the scale. These have
+a really "fun" tactile bump, with almost no pre-travel. I don't think
+it requires a lot of force for the bump, but since the bump is so
+sharp it may feel heavier than it is. I find it hard not to bottom out
+when using these switches.
+
+Soundwise, these can sound quite inconsistent (stock), and some
+switches have really annoying ping.
+
+I do not think I will be using them for a full build, but I enjoy
+having this switch on some of designated keys, maybe return or the
+F-keys?
+
+**Tecsee Sapphire**
+
+Mid-strength tactile. Has a nice bumb and and very smooth travel
+afterwards. Cannot really say anything bad about it. The sound may be
+too high pitched for the connoisseurs, but I do not mind too much.
+
+**Gateron Brown**
+
+Hated among many. I actually do not think it is too bad, but it does
+require lubing to sound more tolerable. Not a fan of such a "light"
+tactile signature tho.
+
+**Cherry MX Brown**
+
+TBD
+
+**Frankenswitches**
+
+- Glorious Boba (?): Glorious Panda stem in Boba housing. Feels like
+Glorious Panda with less pre-travel and easier bottom-out. Sounds
+quite similar.
+
+# Linear
+
+**Gateron Red**
+
+Linear switch. A bit too smooth for my taste. It feels like for some
+of these switches the actuation point is really close. I sometimes
+accidentally triggered a switch when i was resting my fingers on the
+keyboard.
+
+Can be very clacky, but sound is drastically improved with a tape mod.
+
+**Gazzew Bobagum**
+
+Silent linear, 62g. Nice linear switch, smooth, but with a good amount
+of force. Produce very little sound.