jonaprieto

% -------------------------------------------------------------------
% Paragraph numbering
% -------------------------------------------------------------------

\usepackage{parano}% http://www.sci.usq.edu.au/staff/braithwa/parano.sty
%\usepackage{hyperref}

%Fixes to parano.sty. One must uses the command \parano.
\makeatletter
\newcommand{\paranospace}{\hfill}% Introduced for more flexible customisation

jonaprieto

Example 1: House Graph

HouseGraph = Graph[{
    1 -> 2,
    1 -> 3,
    2 -> 3,
    2 -> 4,
    3 -> 5,
    4 -> 5

jonaprieto

module Juvix.Compiler.Backend.Geb.Normalisation
  ( module Juvix.Compiler.Backend.Geb.Evaluator,
    module Juvix.Compiler.Backend.Geb.Evaluator.Options,
  )
where

import Data.List.NonEmpty
import Juvix.Compiler.Backend.Geb.Evaluator.Options
import Juvix.Compiler.Backend.Geb.Language qualified as Geb
import Juvix.Prelude

jonaprieto

title	On planarity of univalent graphs

{-# OPTIONS --without-K --exact-split --allow-unsolved-metas --rewriting #-}

module lib.graph-families.CycleGraph.Faces
  where
  open import foundations.Core

jonaprieto

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

module lib.graph-embeddings.Planar.InductiveDef where
open import foundations.Core

open import lib.graph-definitions.Graph
open Graph
open import lib.graph-walks.Walk

jonaprieto

{-# OPTIONS --cubical --rewriting #-}

module _ where

open import Cubical.Core.Everything
  using (_∧_; _∨_;  ~_; i0;i1 ; transp; Σ; fst; snd
        ; Glue ; glue ; unglue ; lineToEquiv;
        _≃_; _,_)

open import Cubical.Foundations.Prelude

jonaprieto

{-# OPTIONS --cubical --rewriting #-}

module cubical.Univalence where

open import Cubical.Core.Everything
  using (_∧_; _∨_;  ~_; i0;i1 ; transp; Σ; fst; snd
        ; Glue ; glue ; unglue ; lineToEquiv)
  renaming (_≃_ to _≃c_; _,_ to _,c_)

open import Cubical.Foundations.Prelude

jonaprieto

\tableofcontents

Intro

Imports

{-# OPTIONS --with-K --exact-split #-}
module content where

jonaprieto

module _ where

open import Relation.Binary.PropositionalEquality
  using (_≡_; refl)

open import Data.Nat
  using (ℕ; zero; suc)

open import Data.Empty
  using (⊥; ⊥-elim)

jonaprieto

{
	"set type": {
		"prefix": "se",
		"body": "Set ${1|ℓ,ℓ₁,ℓ₂,ℓᵢ,ℓⱼ,lsuc ?,lzero|}",
		"description": "Set type"
	},
	"Type type": {
		"prefix": "ty",
		"body": "Type ${1|ℓ,ℓ₁,ℓ₂,ℓᵢ,ℓⱼ,lsuc ?,lzero|}",
		"description": "Type type"