jonaprieto

Keybase proof

I hereby claim:

• I am jonaprieto on github.
• I am jonaprieto (https://keybase.io/jonaprieto) on keybase.
• I have a public key ASDuCgVOy3BZL6z_PKSQ_YBq0K6S3HcTKdKupJb0pX-aKwo

To claim this, I am signing this object:

jonaprieto

import re

from pathlib import Path

import os
import sys

tex = [i for i in list(Path("latex/").glob('*.tex'))]
latexTags = []

jonaprieto

import sys
import turtle


# -- Settings

sys.setrecursionlimit(100000)

wn = turtle.Screen()
wn.bgcolor('black')

jonaprieto

Norsk Quizlets:

• Vaklner's tekster: https://quizlet.com/Valkner/folders/basar-tekster/sets

• Verbs

  • https://quizlet.com/275768622/norwegian-verbs-flash-cards/
  • https://quizlet.com/285298973/setningsadverb-flash-cards/

• 1000 words: https://quizlet.com/276514199/1000-most-common-norwegian-words-flash-cards/

jonaprieto

module Non-dependent-funext-implies-general-funext where
  open import BasicFunctions
  open import TransportLemmas
  open import EquivalenceType
  open import QuasiinverseType
  open import QuasiinverseLemmas
  open import HLevelTypes
  open import HLevelLemmas
  open import UnivalenceAxiom
  open import CoproductIdentities

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"

jonaprieto

\tableofcontents

Intro

Imports

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

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

{-# 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