transport and hcomp

[lunalunaa]

Implement the following primitives:

• coe (A: I -> Type) (phi: I): A 0 -> A 1 (need to check the freezing condition)
• coeFill (A: I -> Type) (phi: I) (u0: A 0) : Path A u (coe A phi u)
• coeInv
• coeFillInv
• forward (A: I -> Type) (r: I) (u: A r): A 1
• hcomp {A: Type} {phi: I} (u: I -> Partial phi A) (u0: A): A (need to check cubical subtype $\Gamma\vdash u_0: A[\phi \mapsto u\ 0]$)
• hfill {A: Type} {phi: I} (u: I -> Partial phi A) (u0: A): I -> A (need to check cubical subtype condition for u0)
• comp {phi: I} (A: Type) (u: I -> Partial phi A) (u0: A 0): A 1 (need to check cubical subtype condition for u0)

I will ignore the subtype checks before cubical subtype is implemented in another PR. After cubical subtype is finished we just need to change the signatures and add proper inS and outS.

TODO: explore ways to automatically insert inS and outS.

Update (2022 Oct 23): coeFill, coeInv, coeFillInv, forward, hfill, comp will not be implemented as primitives. Instead they are helper functions

This pull request closes #522, #525.

[codecov]

Codecov Report

Merging #539 (2e7c4ec) into main (5ecd681) will decrease coverage by 0.56%.
The diff coverage is 10.00%.

@@             Coverage Diff              @@
##               main     #539      +/-   ##
============================================
- Coverage     80.54%   79.98%   -0.57%     
- Complexity     2750     2751       +1     
============================================
  Files           224      224              
  Lines          8637     8705      +68     
  Branches       1071     1072       +1     
============================================
+ Hits           6957     6963       +6     
- Misses         1097     1159      +62     
  Partials        583      583              

Impacted Files	Coverage Δ
...e/src/main/java/org/aya/core/serde/Serializer.java	90.07% <0.00%> (-0.70%)	⬇️
base/src/main/java/org/aya/core/term/PrimTerm.java	73.33% <0.00%> (-5.24%)	⬇️
base/src/main/java/org/aya/core/term/Term.java	96.31% <0.00%> (-0.60%)	⬇️
...e/src/main/java/org/aya/distill/CoreDistiller.java	79.12% <0.00%> (-0.39%)	⬇️
base/src/main/java/org/aya/tyck/LittleTyper.java	66.17% <0.00%> (-0.99%)	⬇️
...c/main/java/org/aya/core/visitor/BetaExpander.java	40.84% <6.81%> (-52.02%)	⬇️
base/src/main/java/org/aya/core/def/PrimDef.java	81.67% <19.04%> (-12.02%)	⬇️

Help us with your feedback. Take ten seconds to tell us how you rate us. Have a feature suggestion? Share it here.

[ice1000]

Are you sure that we need hfill as primitive? I think it can be implemented in terms of hcomp and cubical subtype

[ice1000]

Congratulations!!