No. postulates: 16

--------------------------------------------------------------------------------
./../src/foundations/BasicEquivalences.lagda.md:
(L40)
∑-+-≃-+-∑ -- TODO: prove this in another time, np.
  : ∀ {ℓ₁ ℓ₂ ℓ₃} {X : Type ℓ₁}{A : X → Type ℓ₂}{B : X → Type ℓ₃}
  → (∑[ x ∶ X ] (A x + B x)) ≃ ((∑[ x ∶ X ] (A x)) + (∑[ x ∶ X ] (B x)) )

--------------------------------------------------------------------------------
./../src/foundations/FunExtAxiom.lagda.md:
(L40)
axiomFunExt : isEquiv happly

--------------------------------------------------------------------------------
./../src/foundations/Rewriting.lagda.md:
(L20)
_↦_
  : ∀ {ℓ : Level}{A : Type ℓ}
  → A → A
  → Type ℓ

--------------------------------------------------------------------------------
./../src/foundations/TruncationType.lagda.md:
(L81)
trunc : ∀ {ℓ} {A : Type ℓ} → isProp ∥ A ∥

--------------------------------------------------------------------------------
./../src/foundations/UnivalenceAxiom.lagda.md:
(L53)
axiomUnivalence : isEquivalence idtoeqv

--------------------------------------------------------------------------------
./../src/lib/graph-embeddings/HIT.lagda.md:
(L22)
runit
  : ∀ {ℓ : Level}{A : Type ℓ} {a a' : A}{p : a ≡ a'}
  → p · idp ↦ p

(L78)
𝔾 : Type ℓ
-- 0-cells
𝕟 : Node G → 𝔾
-- 1-cells
𝕖 : ∀ {x y : Node G} → Edge G x y → 𝕟 x ≡ 𝕟 y
-- 2-cells
𝕨 = to-eq 𝕟 𝕖
postulate
𝕗 : (F : Face G 𝕄)
  → (a b : Node (Face.A F))
  -- ─────────────────────────────────────
  → 𝕨 (cw-walk F a b) ≡ 𝕨 (ccw-walk F a b)

(L86)
𝕗 : (F : Face G 𝕄)
  → (a b : Node (Face.A F))
  -- ─────────────────────────────────────
  → 𝕨 (cw-walk F a b) ≡ 𝕨 (ccw-walk F a b)

(L109)
𝔾-rec : 𝔾 → A

(L118)
𝔾-β-rec-edges
  : ∀ {x y : Node G}
  → (e : Edge G x y)
  -- ───────────────────────
  → ap 𝔾-rec (𝕖 e) ↦ (A-𝕖 e)
  {-# REWRITE 𝔾-β-rec-edges #-}

(L146)
𝔾-β-rec-faces
  : (F : Face G 𝕄) → (a b : Node (Face.A F))
  -- ──────────────────────────────────────────────────────
  → ap (ap 𝔾-rec) (𝕗 F a b)
  ≡ lhs (cw-walk F a b) · A-𝕗 F a b · ! lhs (ccw-walk F a b)

(L197)
𝔾-ind : (x : 𝔾) → A x
𝔾-β-ind-nodes
  : (x : Node G)
  -- ──────────────────
  → 𝔾-ind (𝕟 x) ↦ A-𝕟 x

(L206)
𝔾-β-ind-edges
  : ∀ {x y : Node G}
  → (e : Edge G x y)
  -- ─────────────────────
  → apd 𝔾-ind (𝕖 e) ↦ A-𝕖 e

(L278)
𝔾-β-ind-faces : apd² 𝔾-ind (𝕗 F a b) ≡ A-𝕗-F-a-b
-- {-# REWRITE 𝔾-β-ind-faces #-}

--------------------------------------------------------------------------------
./../src/lib/graph-embeddings/HIT/toProp.lagda.md:
(L46)
𝔾-rec : 𝔾 → A
𝔾-β-rec-nodes : (x : Node G) → 𝔾-rec (𝕟 x) ↦ A-𝕟 x
{-# REWRITE 𝔾-β-rec-nodes #-}

(L59)
𝔾-β-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)))
  -}

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