File tree Expand file tree Collapse file tree 4 files changed +18
-17
lines changed
Expand file tree Collapse file tree 4 files changed +18
-17
lines changed Original file line number Diff line number Diff line change 4343 < a id ="1296 " class ="Number "> 2</ a > < a id ="1298 " href ="Cubical.Algebra.CommSemiring.Base.html#657 " class ="Function Operator "> ·</ a > < a id ="1300 " class ="Symbol "> (</ a > < a id ="1301 " href ="Cubical.Algebra.Semiring.BigOps.html#755 " class ="Function "> ∑</ a > < a id ="1303 " class ="Symbol "> (</ a > < a id ="1304 " href ="Cubical.Data.Nat.Triangular.html#782 " class ="Function "> first</ a > < a id ="1310 " class ="Symbol "> (</ a > < a id ="1311 " class ="Number "> 2</ a > < a id ="1313 " href ="Cubical.Algebra.CommSemiring.Base.html#633 " class ="Function Operator "> +</ a > < a id ="1315 " href ="Cubical.Data.Nat.Triangular.html#1125 " class ="Bound "> n</ a > < a id ="1316 " class ="Symbol "> )</ a > < a id ="1318 " href ="Cubical.Foundations.Function.html#898 " class ="Function Operator "> ∘</ a > < a id ="1320 " href ="Cubical.Data.FinData.Base.html#1001 " class ="Function "> weakenFin</ a > < a id ="1329 " class ="Symbol "> )</ a > < a id ="1331 " href ="Cubical.Algebra.CommSemiring.Base.html#633 " class ="Function Operator "> +</ a > < a id ="1333 " class ="Symbol "> (</ a > < a id ="1334 " href ="Agda.Builtin.Nat.html#234 " class ="InductiveConstructor "> suc</ a > < a id ="1338 " href ="Cubical.Data.Nat.Triangular.html#1125 " class ="Bound "> n</ a > < a id ="1339 " class ="Symbol "> ))</ a > < a id ="1365 " href ="Cubical.Foundations.Prelude.html#9029 " class ="Function "> ≡⟨</ a > < a id ="1368 " href ="Cubical.Data.Nat.Triangular.html#1842 " class ="Function "> step2</ a > < a id ="1374 " href ="Cubical.Foundations.Prelude.html#9029 " class ="Function "> ⟩</ a >
4444 < a id ="1378 " class ="Number "> 2</ a > < a id ="1380 " href ="Cubical.Algebra.CommSemiring.Base.html#657 " class ="Function Operator "> ·</ a > < a id ="1382 " class ="Symbol "> (</ a > < a id ="1383 " href ="Cubical.Algebra.Semiring.BigOps.html#755 " class ="Function "> ∑</ a > < a id ="1385 " class ="Symbol "> (</ a > < a id ="1386 " href ="Cubical.Data.Nat.Triangular.html#782 " class ="Function "> first</ a > < a id ="1392 " class ="Symbol "> (</ a > < a id ="1393 " class ="Number "> 1</ a > < a id ="1395 " href ="Cubical.Algebra.CommSemiring.Base.html#633 " class ="Function Operator "> +</ a > < a id ="1397 " href ="Cubical.Data.Nat.Triangular.html#1125 " class ="Bound "> n</ a > < a id ="1398 " class ="Symbol "> ))</ a > < a id ="1401 " href ="Cubical.Algebra.CommSemiring.Base.html#633 " class ="Function Operator "> +</ a > < a id ="1403 " class ="Symbol "> (</ a > < a id ="1404 " href ="Agda.Builtin.Nat.html#234 " class ="InductiveConstructor "> suc</ a > < a id ="1408 " href ="Cubical.Data.Nat.Triangular.html#1125 " class ="Bound "> n</ a > < a id ="1409 " class ="Symbol "> ))</ a > < a id ="1447 " href ="Cubical.Foundations.Prelude.html#9029 " class ="Function "> ≡⟨</ a > < a id ="1450 " href ="Cubical.Data.Nat.Triangular.html#1914 " class ="Function "> step3</ a > < a id ="1456 " href ="Cubical.Foundations.Prelude.html#9029 " class ="Function "> ⟩</ a >
4545 < a id ="1460 " class ="Number "> 2</ a > < a id ="1462 " href ="Cubical.Algebra.CommSemiring.Base.html#657 " class ="Function Operator "> ·</ a > < a id ="1464 " href ="Cubical.Algebra.Semiring.BigOps.html#755 " class ="Function "> ∑</ a > < a id ="1466 " class ="Symbol "> (</ a > < a id ="1467 " href ="Cubical.Data.Nat.Triangular.html#782 " class ="Function "> first</ a > < a id ="1473 " class ="Symbol "> (</ a > < a id ="1474 " class ="Number "> 1</ a > < a id ="1476 " href ="Cubical.Algebra.CommSemiring.Base.html#633 " class ="Function Operator "> +</ a > < a id ="1478 " href ="Cubical.Data.Nat.Triangular.html#1125 " class ="Bound "> n</ a > < a id ="1479 " class ="Symbol "> ))</ a > < a id ="1482 " href ="Cubical.Algebra.CommSemiring.Base.html#633 " class ="Function Operator "> +</ a > < a id ="1484 " class ="Number "> 2</ a > < a id ="1486 " href ="Cubical.Algebra.CommSemiring.Base.html#657 " class ="Function Operator "> ·</ a > < a id ="1488 " class ="Symbol "> (</ a > < a id ="1489 " href ="Agda.Builtin.Nat.html#234 " class ="InductiveConstructor "> suc</ a > < a id ="1493 " href ="Cubical.Data.Nat.Triangular.html#1125 " class ="Bound "> n</ a > < a id ="1494 " class ="Symbol "> )</ a > < a id ="1529 " href ="Cubical.Foundations.Prelude.html#9029 " class ="Function "> ≡⟨</ a > < a id ="1532 " href ="Cubical.Data.Nat.Triangular.html#1964 " class ="Function "> step4</ a > < a id ="1538 " href ="Cubical.Foundations.Prelude.html#9029 " class ="Function "> ⟩</ a >
46- < a id ="1542 " href ="Cubical.Data.Nat.Triangular.html#1125 " class ="Bound "> n</ a > < a id ="1544 " href ="Cubical.Algebra.CommSemiring.Base.html#657 " class ="Function Operator "> ·</ a > < a id ="1546 " class ="Symbol "> (</ a > < a id ="1547 " href ="Cubical.Data.Nat.Triangular.html#1125 " class ="Bound "> n</ a > < a id ="1549 " href ="Cubical.Algebra.CommSemiring.Base.html#633 " class ="Function Operator "> +</ a > < a id ="1551 " class ="Number "> 1</ a > < a id ="1552 " class ="Symbol "> )</ a > < a id ="1554 " href ="Cubical.Algebra.CommSemiring.Base.html#633 " class ="Function Operator "> +</ a > < a id ="1556 " class ="Number "> 2</ a > < a id ="1558 " href ="Cubical.Algebra.CommSemiring.Base.html#657 " class ="Function Operator "> ·</ a > < a id ="1560 " class ="Symbol "> (</ a > < a id ="1561 " href ="Agda.Builtin.Nat.html#234 " class ="InductiveConstructor "> suc</ a > < a id ="1565 " href ="Cubical.Data.Nat.Triangular.html#1125 " class ="Bound "> n</ a > < a id ="1566 " class ="Symbol "> )</ a > < a id ="1611 " href ="Cubical.Foundations.Prelude.html#9029 " class ="Function "> ≡⟨</ a > < a id ="1614 " href ="Cubical.Tactics.NatSolver.Reflection.html#4224 " class ="Macro "> solveℕ!</ a > < a id ="1622 " href ="Cubical.Foundations.Prelude.html#9029 " class ="Function "> ⟩</ a >
46+ < a id ="1542 " href ="Cubical.Data.Nat.Triangular.html#1125 " class ="Bound "> n</ a > < a id ="1544 " href ="Cubical.Algebra.CommSemiring.Base.html#657 " class ="Function Operator "> ·</ a > < a id ="1546 " class ="Symbol "> (</ a > < a id ="1547 " href ="Cubical.Data.Nat.Triangular.html#1125 " class ="Bound "> n</ a > < a id ="1549 " href ="Cubical.Algebra.CommSemiring.Base.html#633 " class ="Function Operator "> +</ a > < a id ="1551 " class ="Number "> 1</ a > < a id ="1552 " class ="Symbol "> )</ a > < a id ="1554 " href ="Cubical.Algebra.CommSemiring.Base.html#633 " class ="Function Operator "> +</ a > < a id ="1556 " class ="Number "> 2</ a > < a id ="1558 " href ="Cubical.Algebra.CommSemiring.Base.html#657 " class ="Function Operator "> ·</ a > < a id ="1560 " class ="Symbol "> (</ a > < a id ="1561 " href ="Agda.Builtin.Nat.html#234 " class ="InductiveConstructor "> suc</ a > < a id ="1565 " href ="Cubical.Data.Nat.Triangular.html#1125 " class ="Bound "> n</ a > < a id ="1566 " class ="Symbol "> )</ a > < a id ="1611 " href ="Cubical.Foundations.Prelude.html#9029 " class ="Function "> ≡⟨</ a > < a id ="1614 " href ="Cubical.Tactics.NatSolver.Reflection.html#4249 " class ="Macro "> solveℕ!</ a > < a id ="1622 " href ="Cubical.Foundations.Prelude.html#9029 " class ="Function "> ⟩</ a >
4747 < a id ="1626 " class ="Symbol "> (</ a > < a id ="1627 " href ="Agda.Builtin.Nat.html#234 " class ="InductiveConstructor "> suc</ a > < a id ="1631 " href ="Cubical.Data.Nat.Triangular.html#1125 " class ="Bound "> n</ a > < a id ="1632 " class ="Symbol "> )</ a > < a id ="1634 " href ="Cubical.Algebra.CommSemiring.Base.html#657 " class ="Function Operator "> ·</ a > < a id ="1636 " class ="Symbol "> (</ a > < a id ="1637 " href ="Agda.Builtin.Nat.html#234 " class ="InductiveConstructor "> suc</ a > < a id ="1641 " class ="Symbol "> (</ a > < a id ="1642 " href ="Cubical.Data.Nat.Triangular.html#1125 " class ="Bound "> n</ a > < a id ="1644 " href ="Cubical.Algebra.CommSemiring.Base.html#633 " class ="Function Operator "> +</ a > < a id ="1646 " class ="Number "> 1</ a > < a id ="1647 " class ="Symbol "> ))</ a > < a id ="1695 " href ="Cubical.Foundations.Prelude.html#9576 " class ="Function Operator "> ∎</ a >
4848 < a id ="1699 " class ="Keyword "> where</ a >
4949 < a id ="1709 " href ="Cubical.Data.Nat.Triangular.html#1709 " class ="Function "> step0</ a > < a id ="1715 " class ="Symbol "> =</ a > < a id ="1717 " href ="Cubical.Foundations.Prelude.html#1407 " class ="Function "> cong</ a > < a id ="1722 " class ="Symbol "> (λ</ a > < a id ="1725 " href ="Cubical.Data.Nat.Triangular.html#1725 " class ="Bound "> u</ a > < a id ="1727 " class ="Symbol "> →</ a > < a id ="1729 " class ="Number "> 2</ a > < a id ="1731 " href ="Cubical.Algebra.CommSemiring.Base.html#657 " class ="Function Operator "> ·</ a > < a id ="1733 " href ="Cubical.Data.Nat.Triangular.html#1725 " class ="Bound "> u</ a > < a id ="1734 " class ="Symbol "> )</ a > < a id ="1736 " class ="Symbol "> (</ a > < a id ="1737 " href ="Cubical.Algebra.Semiring.BigOps.html#844 " class ="Function "> ∑Last</ a > < a id ="1743 " class ="Symbol "> (</ a > < a id ="1744 " href ="Cubical.Data.Nat.Triangular.html#782 " class ="Function "> first</ a > < a id ="1750 " class ="Symbol "> (</ a > < a id ="1751 " class ="Number "> 2</ a > < a id ="1753 " href ="Cubical.Algebra.CommSemiring.Base.html#633 " class ="Function Operator "> +</ a > < a id ="1755 " href ="Cubical.Data.Nat.Triangular.html#1125 " class ="Bound "> n</ a > < a id ="1756 " class ="Symbol "> )))</ a >
Original file line number Diff line number Diff line change 247247 < a id ="8183 " class ="Symbol "> (</ a > < a id ="8184 " href ="Cubical.Homotopy.Connected.html#13053 " class ="Function "> isEquiv→isConnected</ a > < a id ="8204 " class ="Symbol "> _</ a > < a id ="8206 " class ="Symbol "> (</ a > < a id ="8207 " href ="Cubical.HITs.James.Inductive.PushoutFormula.html#6424 " class ="Function "> 𝕁amesPush≃</ a > < a id ="8218 " href ="Cubical.HITs.James.Inductive.PushoutFormula.html#7850 " class ="Bound "> k</ a > < a id ="8220 " class ="Symbol "> .</ a > < a id ="8221 " href ="Agda.Builtin.Sigma.html#263 " class ="Field "> snd</ a > < a id ="8224 " class ="Symbol "> )</ a > < a id ="8226 " class ="Symbol "> _)))))</ a >
248248
249249 < a id ="8238 " href ="Cubical.HITs.James.Inductive.PushoutFormula.html#8238 " class ="Function "> nat-path</ a > < a id ="8247 " class ="Symbol "> :</ a > < a id ="8249 " class ="Symbol "> (</ a > < a id ="8250 " href ="Cubical.HITs.James.Inductive.PushoutFormula.html#8250 " class ="Bound "> n</ a > < a id ="8252 " href ="Cubical.HITs.James.Inductive.PushoutFormula.html#8252 " class ="Bound "> m</ a > < a id ="8254 " href ="Cubical.HITs.James.Inductive.PushoutFormula.html#8254 " class ="Bound "> k</ a > < a id ="8256 " class ="Symbol "> :</ a > < a id ="8258 " href ="Agda.Builtin.Nat.html#203 " class ="Datatype "> ℕ</ a > < a id ="8259 " class ="Symbol "> )</ a > < a id ="8261 " class ="Symbol "> →</ a > < a id ="8263 " class ="Symbol "> (</ a > < a id ="8264 " class ="Number "> 1</ a > < a id ="8266 " href ="Agda.Builtin.Nat.html#336 " class ="Primitive Operator "> +</ a > < a id ="8268 " class ="Symbol "> (</ a > < a id ="8269 " href ="Cubical.HITs.James.Inductive.PushoutFormula.html#8254 " class ="Bound "> k</ a > < a id ="8271 " href ="Agda.Builtin.Nat.html#336 " class ="Primitive Operator "> +</ a > < a id ="8273 " href ="Cubical.HITs.James.Inductive.PushoutFormula.html#8252 " class ="Bound "> m</ a > < a id ="8274 " class ="Symbol "> ))</ a > < a id ="8277 " href ="Cubical.Data.Nat.Base.html#172 " class ="Primitive Operator "> ·</ a > < a id ="8279 " href ="Cubical.HITs.James.Inductive.PushoutFormula.html#8250 " class ="Bound "> n</ a > < a id ="8281 " href ="Agda.Builtin.Cubical.Path.html#272 " class ="Function Operator "> ≡</ a > < a id ="8283 " href ="Cubical.HITs.James.Inductive.PushoutFormula.html#8254 " class ="Bound "> k</ a > < a id ="8285 " href ="Cubical.Data.Nat.Base.html#172 " class ="Primitive Operator "> ·</ a > < a id ="8287 " href ="Cubical.HITs.James.Inductive.PushoutFormula.html#8250 " class ="Bound "> n</ a > < a id ="8289 " href ="Agda.Builtin.Nat.html#336 " class ="Primitive Operator "> +</ a > < a id ="8291 " class ="Symbol "> (</ a > < a id ="8292 " class ="Number "> 1</ a > < a id ="8294 " href ="Agda.Builtin.Nat.html#336 " class ="Primitive Operator "> +</ a > < a id ="8296 " href ="Cubical.HITs.James.Inductive.PushoutFormula.html#8252 " class ="Bound "> m</ a > < a id ="8297 " class ="Symbol "> )</ a > < a id ="8299 " href ="Cubical.Data.Nat.Base.html#172 " class ="Primitive Operator "> ·</ a > < a id ="8301 " href ="Cubical.HITs.James.Inductive.PushoutFormula.html#8250 " class ="Bound "> n</ a >
250- < a id ="8307 " href ="Cubical.HITs.James.Inductive.PushoutFormula.html#8238 " class ="Function "> nat-path</ a > < a id ="8316 " class ="Symbol "> _</ a > < a id ="8318 " class ="Symbol "> _</ a > < a id ="8320 " class ="Symbol "> _</ a > < a id ="8322 " class ="Symbol "> =</ a > < a id ="8324 " href ="Cubical.Tactics.NatSolver.Reflection.html#4224 " class ="Macro "> solveℕ!</ a >
250+ < a id ="8307 " href ="Cubical.HITs.James.Inductive.PushoutFormula.html#8238 " class ="Function "> nat-path</ a > < a id ="8316 " class ="Symbol "> _</ a > < a id ="8318 " class ="Symbol "> _</ a > < a id ="8320 " class ="Symbol "> _</ a > < a id ="8322 " class ="Symbol "> =</ a > < a id ="8324 " href ="Cubical.Tactics.NatSolver.Reflection.html#4249 " class ="Macro "> solveℕ!</ a >
251251
252252 < a id ="8335 " class ="Comment "> -- Connectivity results</ a >
253253
Original file line number Diff line number Diff line change 1818
1919< a id ="408 " class ="Keyword "> module</ a > < a id ="ReflectionSolving "> </ a > < a id ="415 " href ="Cubical.Tactics.NatSolver.Examples.html#415 " class ="Module "> ReflectionSolving</ a > < a id ="433 " class ="Symbol "> (</ a > < a id ="434 " href ="Cubical.Tactics.NatSolver.Examples.html#434 " class ="Bound "> x</ a > < a id ="436 " href ="Cubical.Tactics.NatSolver.Examples.html#436 " class ="Bound "> y</ a > < a id ="438 " class ="Symbol "> :</ a > < a id ="440 " href ="Agda.Builtin.Nat.html#203 " class ="Datatype "> ℕ</ a > < a id ="441 " class ="Symbol "> )</ a > < a id ="443 " class ="Keyword "> where</ a >
2020 < a id ="451 " href ="Cubical.Tactics.NatSolver.Examples.html#451 " class ="Function "> _</ a > < a id ="453 " class ="Symbol "> :</ a > < a id ="455 " class ="Symbol "> (</ a > < a id ="456 " href ="Cubical.Tactics.NatSolver.Examples.html#434 " class ="Bound "> x</ a > < a id ="458 " href ="Agda.Builtin.Nat.html#336 " class ="Primitive Operator "> +</ a > < a id ="460 " href ="Cubical.Tactics.NatSolver.Examples.html#436 " class ="Bound "> y</ a > < a id ="461 " class ="Symbol "> )</ a > < a id ="463 " href ="Cubical.Data.Nat.Base.html#172 " class ="Primitive Operator "> ·</ a > < a id ="465 " class ="Symbol "> (</ a > < a id ="466 " href ="Cubical.Tactics.NatSolver.Examples.html#434 " class ="Bound "> x</ a > < a id ="468 " href ="Agda.Builtin.Nat.html#336 " class ="Primitive Operator "> +</ a > < a id ="470 " href ="Cubical.Tactics.NatSolver.Examples.html#436 " class ="Bound "> y</ a > < a id ="471 " class ="Symbol "> )</ a > < a id ="473 " href ="Agda.Builtin.Cubical.Path.html#272 " class ="Function Operator "> ≡</ a > < a id ="475 " href ="Cubical.Tactics.NatSolver.Examples.html#434 " class ="Bound "> x</ a > < a id ="477 " href ="Cubical.Data.Nat.Base.html#172 " class ="Primitive Operator "> ·</ a > < a id ="479 " href ="Cubical.Tactics.NatSolver.Examples.html#434 " class ="Bound "> x</ a > < a id ="481 " href ="Agda.Builtin.Nat.html#336 " class ="Primitive Operator "> +</ a > < a id ="483 " class ="Number "> 2</ a > < a id ="485 " href ="Cubical.Data.Nat.Base.html#172 " class ="Primitive Operator "> ·</ a > < a id ="487 " href ="Cubical.Tactics.NatSolver.Examples.html#434 " class ="Bound "> x</ a > < a id ="489 " href ="Cubical.Data.Nat.Base.html#172 " class ="Primitive Operator "> ·</ a > < a id ="491 " href ="Cubical.Tactics.NatSolver.Examples.html#436 " class ="Bound "> y</ a > < a id ="493 " href ="Agda.Builtin.Nat.html#336 " class ="Primitive Operator "> +</ a > < a id ="495 " href ="Cubical.Tactics.NatSolver.Examples.html#436 " class ="Bound "> y</ a > < a id ="497 " href ="Cubical.Data.Nat.Base.html#172 " class ="Primitive Operator "> ·</ a > < a id ="499 " href ="Cubical.Tactics.NatSolver.Examples.html#436 " class ="Bound "> y</ a >
21- < a id ="503 " class ="Symbol "> _</ a > < a id ="505 " class ="Symbol "> =</ a > < a id ="507 " href ="Cubical.Tactics.NatSolver.Reflection.html#4224 " class ="Macro "> solveℕ!</ a >
21+ < a id ="503 " class ="Symbol "> _</ a > < a id ="505 " class ="Symbol "> =</ a > < a id ="507 " href ="Cubical.Tactics.NatSolver.Reflection.html#4249 " class ="Macro "> solveℕ!</ a >
2222
2323 < a id ="518 " href ="Cubical.Tactics.NatSolver.Examples.html#518 " class ="Function "> _</ a > < a id ="520 " class ="Symbol "> :</ a > < a id ="522 " href ="Agda.Builtin.Nat.html#234 " class ="InductiveConstructor "> suc</ a > < a id ="526 " href ="Cubical.Tactics.NatSolver.Examples.html#434 " class ="Bound "> x</ a > < a id ="528 " href ="Agda.Builtin.Cubical.Path.html#272 " class ="Function Operator "> ≡</ a > < a id ="530 " href ="Cubical.Tactics.NatSolver.Examples.html#434 " class ="Bound "> x</ a > < a id ="532 " href ="Agda.Builtin.Nat.html#336 " class ="Primitive Operator "> +</ a > < a id ="534 " class ="Number "> 1</ a >
24- < a id ="538 " class ="Symbol "> _</ a > < a id ="540 " class ="Symbol "> =</ a > < a id ="542 " href ="Cubical.Tactics.NatSolver.Reflection.html#4224 " class ="Macro "> solveℕ!</ a >
24+ < a id ="538 " class ="Symbol "> _</ a > < a id ="540 " class ="Symbol "> =</ a > < a id ="542 " href ="Cubical.Tactics.NatSolver.Reflection.html#4249 " class ="Macro "> solveℕ!</ a >
2525
2626
2727< a id ="552 " class ="Keyword "> module</ a > < a id ="SolvingExplained "> </ a > < a id ="559 " href ="Cubical.Tactics.NatSolver.Examples.html#559 " class ="Module "> SolvingExplained</ a > < a id ="576 " class ="Keyword "> where</ a >
You can’t perform that action at this time.
0 commit comments