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
Karte der Allgemeinverfügungen zu Schulschließungen oder eingeschränktem Regelbetrieb in Sachsen

SNSZ Karte Datenquelle: Allgemeinverfügungen zu Schulschließungen oder eingeschränktem Regelbetrieb in Sachsen Sächsisches Staatsministerium für Kultu

Jannis Leidel 3 Sep 26, 2022
Ningyu Jia(nj2459)/Mengyin Ma(mm5937) Call Analysis group project(Group 36)

Group and Section Group 36 Section 001 name and UNI Name UNI Ningyu Jia nj2459 Mengyin Ma mm5937 code explanation Parking.py (1) Calculate the rate of

1 Dec 04, 2021
Batch Python Program Verify

Batch Python Program Verify About As a TA(teaching assistant) of Programming Class, it is very annoying to test students' homework assignments one by

Han-Wei Li 7 Dec 20, 2022
Hexa is an advanced browser.It can carry out all the functions present in a browser.

Hexa is an advanced browser.It can carry out all the functions present in a browser.It is coded in the language Python using the modules PyQt5 and sys mainly.It is gonna get developed more in the fut

1 Dec 10, 2021
This is a backport of the BaseExceptionGroup and ExceptionGroup classes from Python 3.11.

This is a backport of the BaseExceptionGroup and ExceptionGroup classes from Python 3.11. It contains the following: The exceptiongroup.BaseExceptionG

Alex Grönholm 19 Dec 15, 2022
Repository for my Monika Assistant project

Monika_Assistant Repository for my Monika Assistant project Major changes: Added face tracker Added manual daily log to see how long it takes me to fi

3 Jan 10, 2022
Advent of Code is an Advent calendar of small programming puzzles for a variety of skill sets and skill levels that can be solved in any programming language you like.

Advent Of Code 2021 - Python English Advent of Code is an Advent calendar of small programming puzzles for a variety of skill sets and skill levels th

Coral Izquierdo Muñiz 2 Jan 09, 2022
Open source home automation that puts local control and privacy first

Home Assistant Open source home automation that puts local control and privacy first. Powered by a worldwide community of tinkerers and DIY enthusiast

Home Assistant 57k Jan 02, 2023
A Tool to validate domestic New Zealand vaccine passes

Vaccine Validator Tool to validate domestic New Zealand vaccine passes Create a new virtual environment: python3 -m venv ./venv Activate virtual envi

8 May 01, 2022
Random pass word generator made with python. PyQt5 module is used to design GUI.

Differences in this GUI program : Default titlebar removed Custom Minimize,Maximize and Close Buttons Drag & move window from any point Program work l

Dimuth De Zoysa 1 Jan 26, 2022
A python tool that creates issues in your repos based on TODO comments in your code

Krypto A neat little sidekick python script to create issues on your repo based on comments left in the code on your behalf Convert todo comments in y

Alex Antoniou 4 Oct 26, 2021
Open-source data observability for modern data teams

Use cases Monitor your data warehouse in minutes: Data anomalies monitoring as dbt tests Data lineage made simple, reliable, and automated dbt operati

889 Jan 01, 2023
This tool for beginner and help those people they gather information about Email Header Analysis, Instagram Information, Instagram Username Check, Ip Information, Phone Number Information, Port Scan

This tool for beginner and help those people they gather information about Email Header Analysis, Instagram Information, Instagram Username Check, Ip Information, Phone Number Information, Port Scan.

cb-kali 5 Feb 18, 2022
Hacking and Learning consistently for 100 days straight af.

#100DaysOfHacking Hacking and Learning consistently for 100 days straight af. [yes, no breaks except mental-break ones, Obviously.] This Repo is one s

FENIL SHAH 17 Sep 09, 2022
An AddOn storing wireguard configuration

Wireguard Database Connector Overview Development Status: 0.1.7 (alpha) First of all, I'd like to thank Jared McKnight for wireguard who inspired me t

Markus Neubauer 3 Dec 30, 2021
WordPress-style shortcodes for Python

Python Shortcodes WordPress-style shortcodes for Python Create and use WordPress-style shortcodes in your Python based app. Example # static output de

Bob 1 Dec 22, 2021
Hospitality app for ERPNext to manage hotels & restaurants.

Hospitality ERPNext Hospitality module is designed to handle workflows for Hotels and Restaurants. Manage Restaurants The Restaurant module in ERPNext

Frappe 19 Dec 26, 2022
Sample microservices application demo

Development mode docker-compose -f docker-compose.yml -f docker-compose.dev.yml up -d or export COMPOSE_FILE='docker-compose.yml:docker-compose.dev.ym

Konstantinos Bairaktaris 1 Nov 14, 2021
Suite of tools for retrieving USGS NWIS observations and evaluating National Water Model (NWM) data.

Documentation OWPHydroTools GitHub pages documentation Motivation We developed OWPHydroTools with data scientists in mind. We attempted to ensure the

36 Dec 11, 2022
Import Apex legends mprt files exported from Legion

Apex-mprt-importer-for-Blender Import Apex legends mprt files exported from Legion. REQUIRES CAST IMPORTER Usage: Use a VPK extracter to extract the m

15 Dec 18, 2022