Ground Zero

This is an attempt to develop Homotopy Type Theory in Lean 4.

As in gebner/hott3, no modifications to the Lean kernel are made, because library uses large eliminator checker ported from Lean 3. So stuff like this will print an error:

hott example {α : Type u} {a b : α} (p q : a = b) : p = q :=
begin cases p; cases q; apply Id.refl end


Most HITs in the library constructed using quotients. Quotients in Lean have good computational properties (Quot.ind computes), so we can define HITs with them without any other changes in Lean’s kernel.

There are:

There are also HITs that cannot be constructed this way. These HITs are defined using standard trick with private structures.

Dependency map

dependency map


Copyright © 2018–2024 Siegmentation Fault <>

Licensed under the Apache License, Version 2.0 (the “License”); you may not use this project except in compliance with the License. You may obtain a copy of the License at

Unless required by applicable law or agreed to in writing, software distributed under the License is distributed on an “AS IS” BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. See the License for the specific language governing permissions and limitations under the License.