Skip to content

Instantly share code, notes, and snippets.

View FrozenWinters's full-sized avatar
🔍
Studying homotopy type theory.

Astra Kolomatskaia FrozenWinters

🔍
Studying homotopy type theory.
70 followers · 8 following
  • Wesleyan University
View GitHub Profile
@FrozenWinters
FrozenWinters / CwF.agda
Last active February 20, 2024 00:20
Categories with Families
{-# OPTIONS --cubical #-}
module CwF where
open import Agda.Primitive using (Level; lzero; lsuc; _⊔_) public
open import Cubical.Core.Everything public
open import Cubical.Foundations.Everything renaming (cong to ap) public
-- Category with Families (4.1.1)
@FrozenWinters
FrozenWinters / weak2cat.agda
Last active March 14, 2023 00:29
Definition of a weak 2-category
{-# OPTIONS --cubical #-}
module weak2cat where
open import Agda.Primitive using (Level; lzero; lsuc; _⊔_) public
open import Cubical.Core.Everything public
open import Cubical.Foundations.Everything public
open import Cubical.Data.Sigma
@FrozenWinters
FrozenWinters / weak-cat.agda
Last active March 13, 2023 21:29
weak and strict 1-categories
{-# OPTIONS --cubical #-}
module weak-cat where
open import Agda.Primitive using (Level; lzero; lsuc; _⊔_) public
open import Cubical.Core.Everything public
open import Cubical.Foundations.Everything public
open import Cubical.Data.Sigma
@FrozenWinters
FrozenWinters / B.agda
Created January 11, 2023 20:24
Constructing a contextual category from a B-system
{-# OPTIONS --cubical --guardedness --rewriting #-}
module B where
open import Agda.Primitive using (Level; lzero; lsuc; _⊔_) public
open import Cubical.Core.Everything public
open import Cubical.Foundations.Everything renaming (cong to ap) public
{-# BUILTIN REWRITE _≡_ #-}
@FrozenWinters
FrozenWinters / modalNbE.agda
Last active November 1, 2022 14:50
NbE for K modal logic
{-# OPTIONS --cubical #-}
module modalNbE where
open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)
open import Cubical.Foundations.Everything renaming (cong to ap)
open import Cubical.Data.Sigma
-- Data Structures
@FrozenWinters
FrozenWinters / untyped-lambda.agda
Created May 11, 2022 17:59
Untyped lambda calculus syntax with explicit substitutions
{-# OPTIONS --cubical --guardedness #-}
module untyped-lambda where
open import Agda.Primitive using (Level; lzero; lsuc; _⊔_) public
open import Cubical.Core.Everything public
open import Cubical.Foundations.Everything renaming (cong to ap) public
open import Cubical.Data.Nat renaming (zero to Z ; suc to S)
@FrozenWinters
FrozenWinters / bsys.agda
Last active April 30, 2022 03:18
B-Systems
{-# OPTIONS --cubical --guardedness #-}
module bsys where
open import Agda.Primitive using (Level; lzero; lsuc; _⊔_) public
open import Cubical.Core.Everything public
open import Cubical.Foundations.Everything renaming (cong to ap) public
-- Definition of a B-system
@FrozenWinters
FrozenWinters / dep.agda
Last active July 27, 2022 16:08
Dependent Multicategories (WIP)
{-# OPTIONS --cubical --guardedness #-}
module dep where
open import Agda.Primitive using (Level; lzero; lsuc; _⊔_) public
open import Cubical.Core.Everything public
open import Cubical.Foundations.Everything renaming (cong to ap) public
private
variable
@FrozenWinters
FrozenWinters / normal.agda
Created March 28, 2022 03:58
Fragment of the proof that normal forms form a set in which I prove that type erasure is injective using a bidirectional approach to sectioning it
module Normal (𝒞 : Contextual ℓ ℓ) ⦃ 𝒞CCC : CCC 𝒞 ⦄
{X : Type ℓ} (base : X → Contextual.ty 𝒞) where
open Contextual 𝒞
open CCC 𝒞CCC
data Ne : (Γ : ctx) (A : ty) → Type ℓ
data Nf : (Γ : ctx) (A : ty) → Type ℓ
data Ne where
VN : {Γ : ctx} {A : ty} → IntVar Γ A → Ne Γ A