package coq-metacoq-quotation

MetaCoq is a meta-programming framework for Coq.

The Quotation module is geared at providing functions □T → □□T for □T := Ast.term (currently implemented) and for □T := { t : Ast.term & Σ ;;; [] |- t : T } (still in the works). Currently Ast.term → Ast.term and (Σ ;;; [] |- t : T) → Ast.term functions are provided for Template and PCUIC terms, in MetaCoq.Quotation.ToTemplate.All and MetaCoq.Quotation.ToPCUIC.All. Proving well-typedness is still a work in progress.

Ultimately the goal of this development is to prove that □ is a lax monoidal semicomonad (a functor with cojoin : □T → □□T that codistributes over unit and ×), which is sufficient for proving Löb's theorem.