Pinned

1. aradarbel10 aradarbel10 Public

   Config files for my GitHub profile.

2. Styff Styff Public

   A functional programming language based on system F (omega) ft. NbE and higher order unification

   OCaml 8

3. A minimalistic example of bidirectio... A minimalistic example of bidirectional type checking for system F

   1

   {-# LANGUAGE StrictData, DerivingVia, OverloadedRecordDot #-}

   2

   3

   {-

   4

     (compiled with GHC 9.4.2)

   5

   -}

4. MyOwnTT MyOwnTT Public

   An example implementation of a dependent type theory in OCaml

   OCaml 9

5. Category of contexts and context-ren... Category of contexts and context-renamings

   1

   ```agda

   2

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

   3

   4

   open import foundation.functions using (_∘_)

   5

   open import foundation.identity-types using (refl; ap) renaming (Id to _≡_)

6. Direct proof for groupoidal structur... Direct proof for groupoidal structure of homotopic identity types via path induction in Agda

   1

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

   2

   3

   import Relation.Binary.PropositionalEquality as Eq

   4

   open Eq using (_≡_; refl)

   5