Isabelle-HoTT/hott, branch master

(broken) update hott for Isabelle 2021-1

2022-06-28T23:28:53+00:00

this just replaces all instance of `this` with instances of `infer`.
Unfortunately, it looks likes something else also broke, and I have
no idea what it is (but the proof for equiv_if_equal fails).

Sadly this means we can't get to univalence for now …
(but rn I'm too tired to try anything else with it)

1. Thm/def statement display. 2. Syntax + computation proof.

2021-06-28T15:06:19+00:00

begin refactoring Equivalence

2021-06-28T12:34:31+00:00

Bad practice huge commit:

2021-06-24T21:40:05+00:00

1. Rudimentary prototype definitional package
2. Started univalence
3. Various compatibility fixes and new theory stubs
4. Updated ROOT file

Patch proof. Now works on Isabelle2021.

2021-04-17T16:41:06+00:00

start hprop stuff

2021-04-10T20:59:42+00:00

rename things + some small changes

2021-01-31T02:54:51+00:00

renamings

2021-01-21T00:52:13+00:00

Swapped notation for metas (now ?) and holes (now {}), other notation and name changes.

2021-01-18T23:49:13+00:00

Basic experiments adding reduction to the type checker

2020-09-23T15:03:42+00:00