Rewriting rules for pushouts

Content created by Fredrik Bakke.

Created on 2024-04-19.
Last modified on 2024-04-19.

{-# OPTIONS --rewriting #-}

module synthetic-homotopy-theory.rewriting-pushouts where
Imports 
open import foundation.homotopies
open import foundation.identity-types
open import foundation.universe-levels

open import reflection.rewriting

open import synthetic-homotopy-theory.cocones-under-spans
open import synthetic-homotopy-theory.dependent-cocones-under-spans
open import synthetic-homotopy-theory.pushouts

Idea

This module endows the eliminator of the standard pushouts cogap with strict computation rules on the point constructors using Agda’s rewriting functionality. This gives the strict equalities

  cogap (inl-pushout f g a) ≐ horizontal-map-cocone f g c a

and

  cogap (inr-pushout f g b) ≐ vertical-map-cocone f g c b.

More generally, strict computation rules for the dependent eliminator are enabled, giving the strict equalities

  dependent-cogap (inl-pushout f g a) ≐
  horizontal-map-dependent-cocone f g (cocone-pushout f g) P c a

and

  dependent-cogap (inr-pushout f g b) ≐
  vertical-map-dependent-cocone f g (cocone-pushout f g) P c b.

In addition, the pre-existing witnesses of these equalities: compute-inl-dependent-cogap, compute-inr-dependent-cogap, and their nondependent counterparts, reduce to refl. This is achieved using Agda’s equality erasure functionality.

To enable these computation rules in your own formalizations, set the --rewriting option and import this module. Keep in mind, however, that we offer no way to selectively disable these rules, so if your module depends on any other module that imports this one, you will automatically also have rewriting for pushouts enabled.

By default, we abstain from using rewrite rules in agda-unimath. However, we recognize their usefulness in, for instance, exploratory formalizations. Since formalizations with and without rewrite rules can coexist, there is no harm in providing these tools for those that see a need to use them. We do, however, emphasize that formalizations without the use of rewrite rules are preferred over those that do use them in the library, as the former can also be applied in other formalizations that do not enable rewrite rules.

Rewrite rules

{-# REWRITE compute-inl-dependent-cogap #-}
{-# REWRITE compute-inr-dependent-cogap #-}

Properties

Verifying the reduction behavior of the computation rules for the eliminators of standard pushouts

module _
  {l1 l2 l3 l4 : Level} {S : UU l1} {A : UU l2} {B : UU l3}
  (f : S → A) (g : S → B) {P : pushout f g → UU l4}
  (d : dependent-cocone f g (cocone-pushout f g) P)
  where

  _ : compute-inl-dependent-cogap f g d ~ refl-htpy
  _ = refl-htpy

  _ : compute-inr-dependent-cogap f g d ~ refl-htpy
  _ = refl-htpy

module _
  {l1 l2 l3 l4 : Level} {S : UU l1} {A : UU l2} {B : UU l3}
  (f : S → A) (g : S → B) {X : UU l4} (c : cocone f g X)
  where

  _ : compute-inl-cogap f g c ~ refl-htpy
  _ = refl-htpy

  _ : compute-inr-cogap f g c ~ refl-htpy
  _ = refl-htpy

See also

  • For some discussion on strict computation rules for higher inductive types, see the introduction to Section 6.2 of [UF13].

References

[UF13]
The Univalent Foundations Program. Homotopy Type Theory: Univalent Foundations of Mathematics. Institute for Advanced Study, 2013. URL: https://homotopytypetheory.org/book/, arXiv:1308.0729.

Recent changes