Spartan implementation of H.O.T.T.

Overview

Down The Path

I was walking down the line,
Trying to find some peace of mind.
Then I saw you,
You were takin' it slow,
And walkin' it one step at a time.

A spartan implementation of H.O.T.T.

Quick Examples

"If you're lost now,
Maybe I could help you along and sing you a song,
And move you on."

I haven't implemented parsers for whole files yet. But I can already parse and print individual terms.

Ordinary MLTT stuff:

λ (t : U) (x : t) => x
Π (t : U) (x : t) => t

Dependent pairs are annotated the type of the second component with a peculiar syntax.

λ (t : U) (x : t) => t { t' => t' } x
Π (t : U) (x : t) Σ (t' : U) => t'

fst and snd are prefixes that have the highest priority, so f fst snd p q stands for (f(fst(snd(p))))(q):

λ (T : U) (S : Π (_ : T) => U) (p : Σ (t : T) => S t) => snd p
Π (T : U) (S : Π (_ : T) => U) (p : Σ (t : T) => S t) => S fst p

ap and Id without dependency:

ap[ . y]
Id[ . A][y, y]

When we deal with n-ary ap and Id, we need to explicitly mark the LHS and RHS of the equations:

ap[z / ap[ . x] : x == x . y]
Id[z / ap[ . x] : x == x . A][y, y]

And of course this one reduces to the one above it.

Type Theory

She said
"I'm looking for a kind of shelter,
No place for me to call my own.
I've been walking all night long, but
I don't know where to call my home."

  • Start out with 0,1,∑,∏,U. (2, Nat are slightly more complicated.)
  • Get to the meat.
    • Typechecking rules for HOTT primitives, which I think should be ap, Id, sym, , .
    • Reduction rules for all those. For simple reduction rules, we should introduce 6 more primitives, which all individially behave well. But that impedes type checking.
  • Inductive types.
  • Higher inductive types.
  • Inductive families.

For inductive types (even 2), we need to make Id, ap stuck on neutral terms. So for instance Id[. A+B][inl a, inl b] would compute to Id[.A][a,b], just as the HoTT book describes. Alternatively we can just make Id compute into a case analysis. Not sure which would be easier.

We might be able to come up with syntactic restrictions on HITs to make it work.

The code files have some comments at the top where you can read a little more about my thoughts.

Implementation

"The only way to find that place is
Close to where my heart is.
I know I'm gonna get there,
But I've got to keep on walking down the line."

Python has got a couple of cool features like assignment expressions and structural pattern matching. I'm trying to write python code in a semi-pure style.

Down the line

I said
"You go on walking down the line,
Wasting all your precious time.
But you're never gonna find it,
Because there is no end to the line,
There's no destination for to find."

(...)

Owner
Trebor Huang
I'm an undergrad at Tsinghua University. / I like mathematics and dependent type theory.
Trebor Huang
API moment - LussovAPI

LussovAPI TL;DR: py API container, pip install -r requirements.txt, example, main configuration Long version: Install Dependancies Download file requi

William Pedersen 1 Nov 30, 2021
Build your own Etherscan with web3.py

Build your own Etherscan with web3.py Video Tutorial: Run it pip3 install -r requirements.txt export FLASK_APP=app export FLASK_ENV=development flask

35 Jan 02, 2023
Python meta class and abstract method library with restrictions.

abcmeta Python meta class and abstract method library with restrictions. This library provides a restricted way to validate abstract methods. The Pyth

Morteza NourelahiAlamdari 8 Dec 14, 2022
PyGo custom language, New but similar language programming

New but similar language programming. Now we are capable to program in a very similar language to Python but at the same time get the efficiency of Go.

Fernando Perez 4 Nov 19, 2022
Union oichecklists For Python

OI Checklist Union Auto-Union user's OI Checklists. Just put your checklist's ID in and it works. How to use it? Put all your OI Checklist IDs (that i

FHVirus 4 Mar 30, 2022
A Curated Collection of Awesome Python Scripts

A Curated Collection of Awesome Python Scripts that will make you go wow. This repository will help you in getting those green squares. Hop in and enjoy the journey of open source. 🚀

Prathima Kadari 248 Dec 31, 2022
Providing a working, flexible, easier and faster installer than the one officially provided by Arch Linux

Purpose The purpose is to bring more people to Arch Linux by providing a working, flexible, easier and faster installer than the one officially provid

André Luís 0 Nov 09, 2022
A Regex based linter tool that works for any language and works exclusively with custom linting rules.

renag Documentation Available Here Short for Regex (re) Nag (like "one who complains"). Now also PEGs (Parsing Expression Grammars) compatible with py

Ryan Peach 12 Oct 20, 2022
Usos Semester average helper

Usos Semester average helper Dzieki temu skryptowi mozesz sprawdzic srednia ocen na kazdy odbyty przez ciebie semestr PARAMETERS required: '--username

2 Jan 17, 2022
Batch obfuscator based on the obfuscation method used by the trick bot launcher

Batch obfuscator based on the obfuscation method used by the trick bot launcher

SlizBinksman 2 Mar 19, 2022
Multiple GNOME terminals in one window

Terminator by Chris Jones [email protected] and others. Description Terminator was

GNOME Terminator 1.5k Jan 01, 2023
Your one and only Discord Bot that helps you concentrate!

Your one and only Discord Bot thats helps you concentrate! Consider leaving a ⭐ if you found the project helpful. concy-bot A bot which constructively

IEEE VIT Student Chapter 22 Sep 27, 2022
The best free and open-source automated time tracker. Cross-platform, extensible, privacy-focused.

Records what you do so that you can know how you've spent your time. All in a secure way where you control the data. Website — Forum — Documentation —

ActivityWatch 7.8k Jan 09, 2023
An open-source Python project series where beginners can contribute and practice coding.

Python Mini Projects A collection of easy Python small projects to help you improve your programming skills. Table Of Contents Aim Of The Project Cont

Leah Nguyen 491 Jan 04, 2023
A very simple boarding app with DRF

CRUD project with DRF A very simple boarding app with DRF. About The Project 유저 정보를 갖고 게시판을 다루는 프로젝트 입니다. Version Python: 3.9 DB: PostgreSQL 13 Django

1 Nov 13, 2021
A reference implementation for processing the content.log files found at opendata.dwd.de/weather

A reference implementation for processing the content.log files found at opendata.dwd.de/weather.

Deutscher Wetterdienst (DWD) 6 Nov 26, 2022
Labspy06 With Python

Labspy06 Profil Nama : Nafal mumtaz fuadi Nim : 312110457 Kelas : T1.21.A.2 Latihan 1 Ubahlah kode dibawah ini menjadi fungsi menggunakan lambda impor

Mas Nafal 1 Dec 12, 2021
A(Sync) Interface for internal Audible API written in pure Python.

Audible Audible is a Python low-level interface to communicate with the non-publicly Audible API. It enables Python developers to create there own Aud

mkb79 192 Jan 03, 2023
Buggy script to play with GPOs

GPOwned /!\ This is a buggy PoC I made just to play with GPOs in my lab. Don't use it in production! /!\ The script uses impacket and ldap3 to update

45 Dec 15, 2022
An example using debezium and mysql with docker-compose

debezium-mysql An example using debezium and mysql with docker-compose The docker compose starts the Zookeeper, Kafka, Mysql and Debezium Connect. Aft

Horácio Dias Baptista Neto 4 May 21, 2022