Presentation

Find one clear goal.

Remember crowd-control.

Leave out: lemPropF

Outline

Introduction

A formalization of Category Theory in cubical Agda.

Cubical Agda: A constructive interpretation of functional extensionality and univalence

Talk about structure of library:

What can I say about reusability?

Meeting with Andrea May 18th

App. 2 in HoTT gives typing rule for pathJ including a computational rule for it.

If you have this computational rule definitionally, then you wouldn't need to use pathJprop.

In discussion-section I mention HITs. I should remove this or come up with a more elaborate example of something you could do, e.g. something with pushouts in the category of sets.

The type Prop is a type where terms are judgmentally equal not just propositionally so.

Maybe mention that Andreas Källberg is working on proving the initiality conjecture.

Intensional Type Theory (ITT): Judgmental equality is decidable

Extensional Type Theory (ETT): Reflection is enough to make judgmental equality undecidable.

Reflection : a ≡ b → a = b

ITT does not have reflections.

HTT ~ ITT + axiomatized univalence Agda ~ ITT + K-rule Coq ~ ITT (no K-rule) Cubical Agda ~ ITT + Path + Glue

Prop is impredicative in Coq (whatever that means)

Prop ≠ hProp

Comments about abstract

Pattern matching for paths (?)

Intro

Main feature of judgmental equality is the conversion rule.

Conor explained: K + eliminators ≡ pat. matching

Explain jugmental equality independently of type-checking

Soundness for equality means that if x = y then x and y must be equal according to the theory/model.

Decidability of = is a necessary condition for typechecking to be decidable.

Canonicity is a nice-to-have though without canonicity terms can get stuck. If we postulate results about judgmental equality. E.g. funext, then we can construct a term of type natural number that is not a numeral. Therefore stating canonicity with natural numbers:

∀ t . ⊢ t : N , ∃ n : N . ⊢ t = sⁿ 0 : N

is a sufficient condition to get a well-behaved equality.

Eta-equality for RawFunctor means that the associative law for functors hold definitionally.

Computational property for funExt is only relevant in two places in my whole formulation. Univalence and gradLemma does not influence any proofs.

2.3 KiB Raw Blame History