Commits

Author Commit Message Labels Comments Date
Paweł Wieczorek
merge with branch, universe is supported
Paweł Wieczorek
cleaning
Branches
universe_dirty_subset
Paweł Wieczorek
Univ finished
Branches
universe_dirty_subset
Paweł Wieczorek
universe almost works
Branches
universe_dirty_subset
Paweł Wieczorek
Universe of small types almost works
Branches
universe_dirty_subset
Paweł Wieczorek
Pi-types are small
Branches
universe_dirty_subset
Paweł Wieczorek
Almost all small types are supported
Branches
universe_dirty_subset
Paweł Wieczorek
Empty and Unit types are now small types
Branches
universe_dirty_subset
Paweł Wieczorek
FundamentalTheorem supports Universe
Branches
universe_dirty_subset
Paweł Wieczorek
ConvertibleToReification supports Universe
Branches
universe_dirty_subset
Paweł Wieczorek
Added NeUniv for ConvertibleToReification
Branches
universe_dirty_subset
Paweł Wieczorek
ConvertibleToReification supports Universe [without NE]
Branches
universe_dirty_subset
Paweł Wieczorek
Strengthened relation for Univ
Branches
universe_dirty_subset_stronger_rel
Paweł Wieczorek
adding univ to LR.CTR, failed
Branches
universe_dirty_subset
Paweł Wieczorek
LR.ConvertibleToReification.Fun supports Universe
Branches
universe_dirty_subset
Paweł Wieczorek
LogReltions.Lift supports Universe
Branches
universe_dirty_subset
Paweł Wieczorek
Syntax.LogRelTmSyntaxStuff supports Universe
Branches
universe_dirty_subset
Paweł Wieczorek
Adding Lift
Branches
universe_dirty_subset
Paweł Wieczorek
LogicalRelations.ContextConversion supports Universe
Branches
universe_dirty_subset
Paweł Wieczorek
LogicalRelations.ProofIrrelevance supports Universe
Branches
universe_dirty_subset
Paweł Wieczorek
LogicalRelations.ClosedUnderPer supports Universe
Branches
universe_dirty_subset
Paweł Wieczorek
LogicalRelations.ClosedUnderConversion supports Univ
Branches
universe_dirty_subset
Paweł Wieczorek
Definition of Logical Relations aligned to Universe; LogicalRelations.Inversion supports Universe
Branches
universe_dirty_subset
Paweł Wieczorek
Aligned to new version of universe in the model
Branches
universe_dirty_subset
Paweł Wieczorek
universe dirty subset
Branches
universe_dirty_subset
Paweł Wieczorek
Removed old NAT_F, added Univ to logical relation
Branches
universe_bigstep
Paweł Wieczorek
Almost working SoJ
Branches
universe_bigstep
Paweł Wieczorek
SoundnessOfJudgements - Fun typ related cases work
Branches
universe_bigstep
Paweł Wieczorek
Aligning SOJ for universe
Branches
universe_bigstep
Paweł Wieczorek
Characterization of PerType works
Branches
universe_bigstep
  1. Prev
  2. Next