Issues

• Proof assistant test: structure identity principle for magmas

  C-metaD-lowI-high
  sinhp/HoTTLean#165 · Filter by author Vtec234 opened on Nov 5, 2025
  17

• Unstructured Id iff Structured Id

  C-model
  sinhp/HoTTLean#158 · Filter by author Jlh18 opened on Oct 24, 2025
  

• MorphismProperty.Over.map preserves pullbacks

  sinhp/HoTTLean#157 · Filter by author Jlh18 opened on Oct 24, 2025

• Beck-chevalley for pi-clans

  C-model
  sinhp/HoTTLean#156 · Filter by author Jlh18 opened on Oct 24, 2025

• Improved mutual induction

  C-metaD-highI-low
  sinhp/HoTTLean#155 · Filter by author Vtec234 opened on Oct 24, 2025

• Look for redundancy in typing rules

  C-syntaxD-unkI-low
  sinhp/HoTTLean#154 · Filter by author Vtec234 opened on Oct 24, 2025

• pi-clan refactor general semantics

  C-model
  sinhp/HoTTLean#149 · Filter by author Jlh18 opened on Sep 26, 2025

• Pi-clan polynomials

  D-highI-critO-poly
  sinhp/HoTTLean#148 · Filter by author Jlh18 opened on Sep 26, 2025
  

• pi-clans refactor

  C-grpdC-modelC-syntaxD-highI-critO-poly
  sinhp/HoTTLean#145 · Filter by author Jlh18 opened on Sep 25, 2025

• Support level polymorphism

  C-metaI-high
  sinhp/HoTTLean#143 · Filter by author Vtec234 opened on Sep 22, 2025
  

• Typechecker optimization

  C-metaI-critO-groupO-help
  sinhp/HoTTLean#142 · Filter by author Vtec234 opened on Sep 22, 2025
  2

• Get rid of level annotations on terms

  C-syntaxD-lowI-low
  sinhp/HoTTLean#119 · Filter by author Vtec234 opened on Aug 4, 2025

• Automate proofs in Model.*.Interpretation more

  C-syntaxD-unkI-low
  sinhp/HoTTLean#50 · Filter by author Vtec234 opened on Feb 12, 2025
  2

• Identify better ways of dealing with intensionality

  D-highI-high
  sinhp/HoTTLean#47 · Filter by author Vtec234 opened on Feb 11, 2025