Astra Kolomatskaia FrozenWinters

🔍

Studying homotopy type theory.

Studies mathematics.

FrozenWinters / kan.ny

Last active March 31, 2026 22:10

The dTT/Narya definition of Kan complexes

	` ------------------------------------------------
	` Kevin Carlson, Astra Kolomatskaia, Reed Mullanix
	` Narya formalisation of Kan complexes
	`
	` developed 13-18 May 2024 during the
	` Prospects of Formal Mathematics
	` trimester program at the
	` Hausdorff Institute for Mathematics
	`
	` dated 7 June 2024

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 / 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 / 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 / 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 / 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 / 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 / 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 / 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 / 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