| CARVIEW |
Select Language
HTTP/2 200
date: Fri, 16 Jan 2026 18:38:18 GMT
content-type: text/html; charset=utf-8
vary: X-PJAX, X-PJAX-Container, Turbo-Visit, Turbo-Frame, X-Requested-With,Accept-Encoding, Accept, X-Requested-With
etag: W/"75eed10fb9a8cbde97cc62c38c17d4cc"
cache-control: max-age=0, private, must-revalidate
strict-transport-security: max-age=31536000; includeSubdomains; preload
x-frame-options: deny
x-content-type-options: nosniff
x-xss-protection: 0
referrer-policy: origin-when-cross-origin, strict-origin-when-cross-origin
content-security-policy: default-src 'none'; base-uri 'self'; child-src github.githubassets.com github.com/assets-cdn/worker/ github.com/assets/ gist.github.com/assets-cdn/worker/; connect-src 'self' uploads.github.com www.githubstatus.com collector.github.com raw.githubusercontent.com api.github.com github-cloud.s3.amazonaws.com github-production-repository-file-5c1aeb.s3.amazonaws.com github-production-upload-manifest-file-7fdce7.s3.amazonaws.com github-production-user-asset-6210df.s3.amazonaws.com *.rel.tunnels.api.visualstudio.com wss://*.rel.tunnels.api.visualstudio.com github.githubassets.com objects-origin.githubusercontent.com copilot-proxy.githubusercontent.com proxy.individual.githubcopilot.com proxy.business.githubcopilot.com proxy.enterprise.githubcopilot.com *.actions.githubusercontent.com wss://*.actions.githubusercontent.com productionresultssa0.blob.core.windows.net/ productionresultssa1.blob.core.windows.net/ productionresultssa2.blob.core.windows.net/ productionresultssa3.blob.core.windows.net/ productionresultssa4.blob.core.windows.net/ productionresultssa5.blob.core.windows.net/ productionresultssa6.blob.core.windows.net/ productionresultssa7.blob.core.windows.net/ productionresultssa8.blob.core.windows.net/ productionresultssa9.blob.core.windows.net/ productionresultssa10.blob.core.windows.net/ productionresultssa11.blob.core.windows.net/ productionresultssa12.blob.core.windows.net/ productionresultssa13.blob.core.windows.net/ productionresultssa14.blob.core.windows.net/ productionresultssa15.blob.core.windows.net/ productionresultssa16.blob.core.windows.net/ productionresultssa17.blob.core.windows.net/ productionresultssa18.blob.core.windows.net/ productionresultssa19.blob.core.windows.net/ github-production-repository-image-32fea6.s3.amazonaws.com github-production-release-asset-2e65be.s3.amazonaws.com insights.github.com wss://alive.github.com wss://alive-staging.github.com api.githubcopilot.com api.individual.githubcopilot.com api.business.githubcopilot.com api.enterprise.githubcopilot.com; font-src github.githubassets.com; form-action 'self' github.com gist.github.com copilot-workspace.githubnext.com objects-origin.githubusercontent.com; frame-ancestors 'none'; frame-src viewscreen.githubusercontent.com notebooks.githubusercontent.com; img-src 'self' data: blob: github.githubassets.com media.githubusercontent.com camo.githubusercontent.com identicons.github.com avatars.githubusercontent.com private-avatars.githubusercontent.com github-cloud.s3.amazonaws.com objects.githubusercontent.com release-assets.githubusercontent.com secured-user-images.githubusercontent.com/ user-images.githubusercontent.com/ private-user-images.githubusercontent.com opengraph.githubassets.com marketplace-screenshots.githubusercontent.com/ copilotprodattachments.blob.core.windows.net/github-production-copilot-attachments/ github-production-user-asset-6210df.s3.amazonaws.com customer-stories-feed.github.com spotlights-feed.github.com objects-origin.githubusercontent.com *.githubusercontent.com; manifest-src 'self'; media-src github.com user-images.githubusercontent.com/ secured-user-images.githubusercontent.com/ private-user-images.githubusercontent.com github-production-user-asset-6210df.s3.amazonaws.com gist.github.com github.githubassets.com; script-src github.githubassets.com; style-src 'unsafe-inline' github.githubassets.com; upgrade-insecure-requests; worker-src github.githubassets.com github.com/assets-cdn/worker/ github.com/assets/ gist.github.com/assets-cdn/worker/
server: github.com
content-encoding: gzip
accept-ranges: bytes
set-cookie: _gh_sess=AKa0eRwvs8mPbGqn5Yfju64OUHvdgzpXE2Xpfz34%2Fq2yylHmg5xZo3zrECPU7NAyaE3k611dqQakzbmndBd9zQl5IZ6EmOe9SWyvkJE%2Bm%2BYlaq2b24mcpHBTFqCHWprnOI4xXooDdpJrcrsS0ZMRI8peVvf4WSnyMrJyPHYIVTXddOx2ke3z%2FGCVNBz9OoRyMs9tqiluBig4XRrco7YrOvAboV%2FLrY13Ygap1I%2BKBqW3waRJzkkoeDSQ6Xa6q3nseebyVNZrYOMqeyUfCRy1iw%3D%3D--XsfD5Acxo7jUdFTW--KXpkL7%2FdwkC%2BpLHKJO1MTA%3D%3D; Path=/; HttpOnly; Secure; SameSite=Lax
set-cookie: _octo=GH1.1.964567753.1768588697; Path=/; Domain=github.com; Expires=Sat, 16 Jan 2027 18:38:17 GMT; Secure; SameSite=Lax
set-cookie: logged_in=no; Path=/; Domain=github.com; Expires=Sat, 16 Jan 2027 18:38:17 GMT; HttpOnly; Secure; SameSite=Lax
x-github-request-id: A8C8:EF25:94B0BE:A5D595:696A8599
yangzhixuan’s gists · GitHub
View GitHub Profile
{{ message }}
Instantly share code, notes, and snippets.
Zhixuan Yang yangzhixuan
-
Imperial College London
- Web
yangzhixuan
/ EasierIndices.agda
Created
September 28, 2025 13:47
Making working with de Brujin indices easier
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| {- | |
| This file demonstrates a technique for making working with de Bruijn-indexed | |
| terms easier that I learnt from the paper /The Linearity Monad/ by Jennifer | |
| Paykin and Steve Zdancewic. After defining well-typed terms `Γ ⊢ τ` using de Bruijn | |
| indices, we define an auxiliary function `lam` that takes in the variable term explicitly: | |
| > lam : {V : Type} {Γ : Cxt V} {τ σ : Ty V} | |
| > → (({Δ : Cxt V} → {{IsExt Δ (Γ , τ)}} → Δ ⊢ τ) | |
| > → (Γ , τ) ⊢ σ) | |
| > → Γ ⊢ τ ⇒ σ |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| \documentclass{article} | |
| \input{numbering.tex} | |
| \begin{document} | |
| \section{Introduction} | |
| \begin{element} | |
| Hello |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| open import Agda.Builtin.Sigma | |
| open import Agda.Builtin.Equality | |
| postulate | |
| funext : ∀ {a b} {A : Set a} {B : A → Set b} → {f g : (x : A) → B x} | |
| → ((x : A) → f x ≡ g x) → f ≡ g | |
| uip : ∀ {a} {A : Set a} {x y : A} → {p q : x ≡ y} → p ≡ q |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| \documentclass{article} | |
| \usepackage{amsmath} | |
| %include polycode.fmt | |
| \newenvironment{autohscode}% | |
| {\relax\ifmmode\expandafter\pmboxed\else\expandafter\plainhscode\fi}% | |
| {\relax\ifmmode\expandafter\endpmboxed\else\expandafter\endplainhscode\fi} |
yangzhixuan
/ MixAlg.hs
Created
January 4, 2024 00:36
Mixing two arbitrary functor algebras (using codensity lifting along the fibration of functor algebras)
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| {-# LANGUAGE ImpredicativeTypes #-} | |
| {-# LANGUAGE GADTs #-} | |
| data Free f a where | |
| V :: a -> Free f a | |
| O :: f (Free f a) -> Free f a | |
| fold :: Functor f => (a -> c) -> (f c -> c) -> Free f a -> c | |
| fold k alg (V a) = k a | |
| fold k alg (O o) = alg (fmap (fold k alg) o) |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| {-# LANGUAGE DataKinds, ImpredicativeTypes #-} | |
| -- Clocked guarded corecursion in the style of Atkey and McBride | |
| -- https://bentnib.org/productive.pdf | |
| -------- Library code ----------- | |
| data Clock | |
| newtype Later (k :: Clock) (a :: *) = L a |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| import Control.Monad (foldM) | |
| import Prelude hiding (sum) | |
| import Control.Monad.Random (MonadRandom(getRandom)) | |
| type Pos = Int | |
| data TArray = E | N TArray -- Left subtree | |
| Int -- Data payload (not position!) | |
| Int -- Priority | |
| Int -- Size of the tree |
yangzhixuan
/ agda.sty
Created
February 24, 2023 20:05
A customised version of agda.sty with some new features: centred code blocks, italic fonts, etc
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| % ---------------------------------------------------------------------- | |
| % Some useful commands when doing highlighting of Agda code in LaTeX. | |
| % ---------------------------------------------------------------------- | |
| \ProvidesPackage{agda} | |
| \RequirePackage{ifxetex, ifluatex, xifthen, xcolor, polytable, etoolbox, | |
| calc, environ, xparse, xkeyval, amsmath} | |
| % https://tex.stackexchange.com/questions/47576/combining-ifxetex-and-ifluatex-with-the-logical-or-operation |
yangzhixuan
/ ndet.rkt
Created
June 4, 2022 08:16
Monadic reflection/reification in Racket using delimited control
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| #lang racket | |
| (require "reflection.rkt") | |
| ; unit : x -> [x] | |
| (define unit (lambda (x) (cons x '()))) | |
| ; bind : [x] -> (x -> [y]) -> [y] | |
| (define bind (lambda (m f) (apply append (map f m)))) |
yangzhixuan
/ AdjointFolds.hs
Last active
March 20, 2022 18:28
A Haskell implementation of adjoint folds and some interface for category theory.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| {-# LANGUAGE KindSignatures, GADTs, TypeOperators, TypeFamilies, UndecidableInstances #-} | |
| {-# LANGUAGE FlexibleContexts, MultiParamTypeClasses, FlexibleInstances #-} | |
| {-# LANGUAGE ConstraintKinds, DeriveFunctor #-} | |
| import Prelude hiding (Functor) | |
| import qualified Prelude (Functor) | |
| -- This file explores doing category theory in Haskell by implementing | |
| -- Ralf Hinze et al.'s adjoint folds [1]: | |
| -- |
NewerOlder
You can’t perform that action at this time.