2.3 KiB
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.