caterwaul

Switch Light/Dark Mode

/caterwaul/Leibniz/groupoid

Copy path to clipboard

Leibniz equality forms a groupoid, with

FIXME: The implementation of inverse forces the target of the functor to be the enriching category. I don’t know if this is fundamentally required, or just a consequence of the common formulations being where everything is π’πžπ­.

Source

{-|
Leibniz equality forms a groupoid, with
- unit = reflexivity,
- product = transitivity, and
- inverse = symmetry.

 **FIXME**: The implementation of `inverse` forces the target of the functor to
 be the enriching category. I don’t know if this is fundamentally required, or
 just a consequence of the common formulations being where everything is π’πžπ­.
-}
let cat = ../Category/Cat/semigroupal

let vObject = Type

let v =
      ../Category/Monoidal/Cartesian/extractMonoidal
        cat
        Type
        vObject
        ../Category/Set/monoidal/cartesian

in  Ξ»(cObject : Kind) β†’
    Ξ»(c : ../Category/Kind cat vObject cObject) β†’
      let dObject = vObject

      let d = ../Category/Monoidal/extractCategory cat Type dObject v

      in  Ξ»(dCategory : ../Category/Type dObject v d) β†’
            let Leibniz = ./Kind cObject dObject c d

            let refl =
                  Ξ»(a : cObject) β†’
                  Ξ»(f : cat.arrow cObject dObject) β†’
                    dCategory.unit (f a)

            let trans =
                  Ξ»(a : { _1 : cObject, _2 : cObject }) β†’
                  Ξ» ( p
                    : βˆ€(r : Type) β†’
                      ( βˆ€(z : cObject) β†’
                        Leibniz.arrow { _1 = z, _2 = a._2 } β†’
                        Leibniz.arrow { _1 = a._1, _2 = z } β†’
                          r
                      ) β†’
                        r
                    ) β†’
                  Ξ»(f : cat.arrow cObject dObject) β†’
                    dCategory.product
                      { _1 = f a._1, _2 = f a._2 }
                      ( Ξ»(r : Type) β†’
                        Ξ» ( arrowsOut
                          : βˆ€(z : dObject) β†’
                            d.arrow { _1 = z, _2 = f a._2 } β†’
                            d.arrow { _1 = f a._1, _2 = z } β†’
                              r
                          ) β†’
                          p
                            r
                            ( Ξ»(z : cObject) β†’
                              Ξ»(g : Leibniz.arrow { _1 = z, _2 = a._2 }) β†’
                              Ξ»(h : Leibniz.arrow { _1 = a._1, _2 = z }) β†’
                                arrowsOut (f z) (g f) (h f)
                            )
                      )

            in    { unit = refl
                  , product = trans
                  , hom.map
                    =
                      Ξ»(a : cat.product cObject cObject) β†’
                      Ξ»(b : cat.product cObject cObject) β†’
                      Ξ» ( f
                        : v.product
                            { _1 = Leibniz.arrow { _1 = b._1, _2 = a._1 }
                            , _2 = Leibniz.arrow { _1 = a._2, _2 = b._2 }
                            }
                        ) β†’
                      Ξ»(fn : Leibniz.arrow a) β†’
                        trans
                          { _1 = b._1, _2 = b._2 }
                          ( Ξ»(r : Type) β†’
                            Ξ» ( arrowsOut
                              : βˆ€(z : cObject) β†’
                                Leibniz.arrow { _1 = z, _2 = b._2 } β†’
                                Leibniz.arrow { _1 = b._1, _2 = z } β†’
                                  r
                              ) β†’
                              arrowsOut
                                a._1
                                ( trans
                                    { _1 = a._1, _2 = b._2 }
                                    ( Ξ»(r : Type) β†’
                                      Ξ» ( arrowsOut
                                        : βˆ€(z : cObject) β†’
                                          Leibniz.arrow { _1 = z, _2 = b._2 } β†’
                                          Leibniz.arrow { _1 = a._1, _2 = z } β†’
                                            r
                                        ) β†’
                                        arrowsOut a._2 f._2 fn
                                    )
                                )
                                f._1
                          )
                  , inverse =
                      Ξ»(a : cat.product cObject cObject) β†’
                      Ξ»(subst : Leibniz.arrow a) β†’
                        subst
                          (Ξ»(x : cObject) β†’ Leibniz.arrow { _1 = x, _2 = a._1 })
                          (refl a._1)
                  }
                : ../Groupoid/Type cObject v Leibniz