lib.graph-embeddings.HIT.toProp.md.

Version of Sunday, January 22, 2023, 10:42 PM

Powered by agda version 2.6.2.2-442c76b and pandoc 2.14.0.3

Investigations on graph-theoretical constructions in Homotopy type theory

Jonathan Prieto-Cubides j.w.w. HΓ₯kon Robbestad Gylterud

Department of Informatics

University of Bergen, Norway

{-# OPTIONS --without-K --exact-split --rewriting #-}

module lib.graph-embeddings.HIT.toProp
  where

  open import foundations.Core
  open import foundations.Rewriting

  open import lib.graph-definitions.Graph
  open Graph

  open import lib.graph-embeddings.Map
  open import lib.graph-embeddings.HIT
  open import lib.graph-walks.Walk
  open import lib.graph-classes.UndirectedGraph
  open import lib.graph-transformations.U

  module
    toProp
    {β„“ : Level}
    (G : Graph β„“)
    (𝕄 : Map G)
    where

    open construction G 𝕄
    open import lib.graph-walks.Walk.Composition
    open βˆ™-walk (U G)

    module
      _
        {β„“β‚‚ : Level}
        (A : Type β„“β‚‚)
        (A-is-prop : isProp A)
        (A-π•Ÿ : (x : Node G) β†’ A)
      where

      A-𝕖 : βˆ€ {x y} β†’ (e : Edge G x y) β†’ A-π•Ÿ x ≑ A-π•Ÿ y
      A-𝕖 {x = x}{y} _ = A-is-prop (A-π•Ÿ x) (A-π•Ÿ y)

      A-𝕨 = to-eq A-π•Ÿ A-𝕖

      postulate
        𝔾-rec : 𝔾 β†’ A
        𝔾-Ξ²-rec-nodes : (x : Node G) β†’ 𝔾-rec (π•Ÿ x) ↦ A-π•Ÿ x
        {-# REWRITE 𝔾-Ξ²-rec-nodes #-}

        𝔾-Ξ²-rec-edges
          : βˆ€ {x y : Node G}
          β†’ (e : Edge G x y) β†’ ap 𝔾-rec (𝕖 e) ↦ A-𝕖 e
        {-# REWRITE 𝔾-Ξ²-rec-edges #-}


      {-
      open GraphFaces {G = G}
      postulate
       𝔾-Ξ²-rec-faces
         : (F : Face map) β†’ (a b : Node (Face.A F))
         β†’ ap (ap 𝔾-rec) (𝕗 F a b)
         ≑ (lhs (ccw-walk F a b) Β· A-𝕗 F a b Β· ! (lhs (cw-walk F a b)))
      -}

    module _ where

      {-
      to-deq'
        : βˆ€ {β„“ : Level} {A : 𝔾 β†’ Type β„“}
        β†’ (f : (x : Node G) β†’ A (π•Ÿ x))
        β†’ (g : βˆ€ {x y : Node G} β†’ (e : Edge G x y)
           β†’ f x ≑ f y [ A ↓ (𝕖 e) ])
        -- ─────────────────────────────────────────────────────────────────
        β†’ {x y : Node G} β†’ (w : Walk x y) β†’ f x ≑ f y [ A ↓ (𝕨 w) ]

      to-deq' = {!!}
      -}

Latest changes

(2022-12-28)(57c278b4) Last updated: 2021-09-16 15:00:00 by jonathan.cubides
(2022-07-06)(d3a4a8cf) minors by jonathan.cubides
(2022-01-26)(4aef326b) [ reports ] added some revisions by jonathan.cubides
(2021-12-20)(049db6a8) Added code of cubical experiments. by jonathan.cubides
(2021-12-20)(961730c9) [ html ] regular update by jonathan.cubides
(2021-12-20)(e0ef9faa) Fixed compilation and format, remove hidden parts by jonathan.cubides
(2021-12-20)(5120e5d1) Added cubical experiment to the master by jonathan.cubides
(2021-12-17)(828fdd0a) More revisions added for CPP by jonathan.cubides
(2021-12-15)(0d6a99d8) Fixed some broken links and descriptions by jonathan.cubides
(2021-12-15)(662a1f2d) [ .gitignore ] add by jonathan.cubides
(2021-12-15)(0630ce66) Minor fixes by jonathan.cubides
(2021-12-13)(04f10eba) Fixed a lot of details by jonathan.cubides
(2021-12-10)(24195c9f) [ .gitignore ] ignore .zip and arxiv related files by jonathan.cubides
(2021-12-09)(538d2859) minor fixes before dinner by jonathan.cubides
(2021-12-09)(36a1a69f) [ planar.pdf ] w.i.p revisions to share on arxiv first by jonathan.cubides