4141< a id ="1102 " class ="Keyword "> open</ a > < a id ="1107 " href ="Cubical.WildCat.BraidedSymmetricMonoidal.html " class ="Module "> WCat3</ a > < a id ="1113 " class ="Keyword "> using</ a > < a id ="1119 " class ="Symbol "> (</ a > < a id ="1120 " href ="Cubical.WildCat.BraidedSymmetricMonoidal.html#484 " class ="Record "> isMonoidalWildCat</ a > < a id ="1137 " class ="Symbol "> )</ a >
4242
4343< a id ="1140 " class ="Comment "> -- Definition 4 (Symmetric Monoidal wild categories)</ a >
44- < a id ="1193 " class ="Keyword "> open</ a > < a id ="1198 " href ="Cubical.WildCat.BraidedSymmetricMonoidal.html " class ="Module "> WCat3</ a > < a id ="1204 " class ="Keyword "> using</ a > < a id ="1210 " class ="Symbol "> (</ a > < a id ="1211 " href ="Cubical.WildCat.BraidedSymmetricMonoidal.html#3196 " class ="Function " > SymmetricMonoidalPrecat </ a > < a id ="1234 " class ="Symbol "> )</ a >
44+ < a id ="1193 " class ="Keyword "> open</ a > < a id ="1198 " href ="Cubical.WildCat.BraidedSymmetricMonoidal.html " class ="Module "> WCat3</ a > < a id ="1204 " class ="Keyword "> using</ a > < a id ="1210 " class ="Symbol "> (</ a > < a id ="1211 " href ="Cubical.WildCat.BraidedSymmetricMonoidal.html#2959 " class ="Record " > isSymmetricWildCat </ a > < a id ="1229 " class ="Symbol "> )</ a >
4545
46- < a id ="1237 " class ="Comment "> --- 2.2 Smash Products</ a >
47- < a id ="1260 " class ="Comment "> -- Definition 5 (Smash products -- note: defined as a coproduct in the</ a >
48- < a id ="1331 " class ="Comment "> -- library. E.g. the ⟨ x , y ⟩ constructor here is simply</ a >
49- < a id ="1389 " class ="Comment "> -- inr(x,y). Also note that pushₗ and pushᵣ are inverted with this</ a >
50- < a id ="1456 " class ="Comment "> -- definition.)</ a >
51- < a id ="1472 " class ="Keyword "> open</ a > < a id ="1477 " href ="Cubical.HITs.SmashProduct.Base.html " class ="Module "> Smash</ a > < a id ="1483 " class ="Keyword "> using</ a > < a id ="1489 " class ="Symbol "> (</ a > < a id ="1490 " href ="Cubical.HITs.SmashProduct.Base.html#2037 " class ="Function Operator "> _⋀_</ a > < a id ="1493 " class ="Symbol "> )</ a >
46+ < a id ="1232 " class ="Comment "> --- 2.2 Smash Products</ a >
47+ < a id ="1255 " class ="Comment "> -- Definition 5 (Smash products -- note: defined as a pushout in the</ a >
48+ < a id ="1324 " class ="Comment "> -- library. E.g. the ⟨ x , y ⟩ constructor here is simply</ a >
49+ < a id ="1382 " class ="Comment "> -- inr(x,y). Also note that pushₗ and pushᵣ are inverted with this</ a >
50+ < a id ="1449 " class ="Comment "> -- definition.)</ a >
51+ < a id ="1465 " class ="Keyword "> open</ a > < a id ="1470 " href ="Cubical.HITs.SmashProduct.Base.html " class ="Module "> Smash</ a > < a id ="1476 " class ="Keyword "> using</ a > < a id ="1482 " class ="Symbol "> (</ a > < a id ="1483 " href ="Cubical.HITs.SmashProduct.Base.html#2037 " class ="Function Operator "> _⋀_</ a > < a id ="1486 " class ="Symbol "> )</ a >
5252
53- < a id ="1496 " class ="Comment "> -- Definition 6 (Functorial action of ⋀)</ a >
54- < a id ="1537 " class ="Keyword "> open</ a > < a id ="1542 " href ="Cubical.HITs.SmashProduct.Base.html " class ="Module "> Smash</ a > < a id ="1548 " class ="Keyword "> using</ a > < a id ="1554 " class ="Symbol "> (</ a > < a id ="1555 " href ="Cubical.HITs.SmashProduct.Base.html#8422 " class ="Function Operator "> _⋀→_</ a > < a id ="1559 " class ="Symbol "> )</ a >
55- < a id ="1561 " class ="Comment "> -- Proposition 7 (Commutativity of ⋀)</ a >
56- < a id ="1599 " class ="Comment "> -- Postponed -- stated as part of Theorem 21</ a >
53+ < a id ="1489 " class ="Comment "> -- Definition 6 (Functorial action of ⋀)</ a >
54+ < a id ="1530 " class ="Keyword "> open</ a > < a id ="1535 " href ="Cubical.HITs.SmashProduct.Base.html " class ="Module "> Smash</ a > < a id ="1541 " class ="Keyword "> using</ a > < a id ="1547 " class ="Symbol "> (</ a > < a id ="1548 " href ="Cubical.HITs.SmashProduct.Base.html#8422 " class ="Function Operator "> _⋀→_</ a > < a id ="1552 " class ="Symbol "> )</ a >
55+ < a id ="1554 " class ="Comment "> -- Proposition 7 (Commutativity of ⋀)</ a >
56+ < a id ="1592 " class ="Comment "> -- Postponed -- stated as part of Theorem 21</ a >
5757
58- < a id ="1645 " class ="Comment "> ---- 3 Associativity ----</ a >
59- < a id ="1671 " class ="Comment "> -- Definition 8 (Double smash product)</ a >
60- < a id ="1710 " class ="Keyword "> open</ a > < a id ="1715 " href ="Cubical.HITs.SmashProduct.Base.html " class ="Module "> Smash</ a > < a id ="1721 " class ="Keyword "> using</ a > < a id ="1727 " class ="Symbol "> (</ a > < a id ="1728 " href ="Cubical.HITs.SmashProduct.Base.html#11856 " class ="Datatype "> ⋀×2</ a > < a id ="1731 " class ="Symbol "> )</ a >
58+ < a id ="1638 " class ="Comment "> ---- 3 Associativity ----</ a >
59+ < a id ="1664 " class ="Comment "> -- Definition 8 (Double smash product)</ a >
60+ < a id ="1703 " class ="Keyword "> open</ a > < a id ="1708 " href ="Cubical.HITs.SmashProduct.Base.html " class ="Module "> Smash</ a > < a id ="1714 " class ="Keyword "> using</ a > < a id ="1720 " class ="Symbol "> (</ a > < a id ="1721 " href ="Cubical.HITs.SmashProduct.Base.html#11856 " class ="Datatype "> ⋀×2</ a > < a id ="1724 " class ="Symbol "> )</ a >
6161
62- < a id ="1734 " class ="Comment "> -- Equivalence between smash product and double smash</ a >
63- < a id ="1788 " class ="Keyword "> open</ a > < a id ="1793 " href ="Cubical.HITs.SmashProduct.Base.html " class ="Module "> Smash</ a > < a id ="1799 " class ="Keyword "> using</ a > < a id ="1805 " class ="Symbol "> (</ a > < a id ="1806 " href ="Cubical.HITs.SmashProduct.Base.html#29187 " class ="Function "> Iso-⋀-⋀×2</ a > < a id ="1815 " class ="Symbol "> )</ a >
62+ < a id ="1727 " class ="Comment "> -- Equivalence between smash product and double smash</ a >
63+ < a id ="1781 " class ="Keyword "> open</ a > < a id ="1786 " href ="Cubical.HITs.SmashProduct.Base.html " class ="Module "> Smash</ a > < a id ="1792 " class ="Keyword "> using</ a > < a id ="1798 " class ="Symbol "> (</ a > < a id ="1799 " href ="Cubical.HITs.SmashProduct.Base.html#29187 " class ="Function "> Iso-⋀-⋀×2</ a > < a id ="1808 " class ="Symbol "> )</ a >
6464
65- < a id ="1818 " class ="Comment "> -- Proposition 9 (Associativity of ⋀)</ a >
66- < a id ="1856 " class ="Comment "> -- Postponed -- stated as part of Theorem 21</ a >
65+ < a id ="1811 " class ="Comment "> -- Proposition 9 (Associativity of ⋀)</ a >
66+ < a id ="1849 " class ="Comment "> -- Postponed -- stated as part of Theorem 21</ a >
6767
68- < a id ="1902 " class ="Comment "> ---- 4 The Heuristic ----</ a >
69- < a id ="1928 " class ="Comment "> -- Lemma 10 (first induction principle for smash products)</ a >
70- < a id ="1987 " class ="Keyword "> open</ a > < a id ="1992 " href ="Cubical.HITs.SmashProduct.Base.html " class ="Module "> Smash</ a > < a id ="1998 " class ="Keyword "> using</ a > < a id ="2004 " class ="Symbol "> (</ a > < a id ="2005 " href ="Cubical.HITs.SmashProduct.Base.html#35827 " class ="Function "> ⋀-fun≡</ a > < a id ="2011 " class ="Symbol "> )</ a >
68+ < a id ="1895 " class ="Comment "> ---- 4 The Heuristic ----</ a >
69+ < a id ="1921 " class ="Comment "> -- Lemma 10 (first induction principle for smash products)</ a >
70+ < a id ="1980 " class ="Keyword "> open</ a > < a id ="1985 " href ="Cubical.HITs.SmashProduct.Base.html " class ="Module "> Smash</ a > < a id ="1991 " class ="Keyword "> using</ a > < a id ="1997 " class ="Symbol "> (</ a > < a id ="1998 " href ="Cubical.HITs.SmashProduct.Base.html#35827 " class ="Function "> ⋀-fun≡</ a > < a id ="2004 " class ="Symbol "> )</ a >
7171
72- < a id ="2014 " class ="Comment "> -- Definition 10</ a >
73- < a id ="2031 " class ="Keyword "> open</ a > < a id ="2036 " href ="Cubical.HITs.SmashProduct.Base.html " class ="Module "> Smash</ a > < a id ="2042 " class ="Keyword "> using</ a > < a id ="2048 " class ="Symbol "> (</ a > < a id ="2049 " href ="Cubical.HITs.SmashProduct.Base.html#35827 " class ="Function "> ⋀-fun≡</ a > < a id ="2055 " class ="Symbol "> )</ a >
72+ < a id ="2007 " class ="Comment "> -- Definition 10</ a >
73+ < a id ="2024 " class ="Keyword "> open</ a > < a id ="2029 " href ="Cubical.HITs.SmashProduct.Base.html " class ="Module "> Smash</ a > < a id ="2035 " class ="Keyword "> using</ a > < a id ="2041 " class ="Symbol "> (</ a > < a id ="2042 " href ="Cubical.HITs.SmashProduct.Base.html#35827 " class ="Function "> ⋀-fun≡</ a > < a id ="2048 " class ="Symbol "> )</ a >
7474
75- < a id ="2058 " class ="Comment "> -- Definition 11 (version using ≡ instead of ≃⋆ is used here)</ a >
76- < a id ="2120 " class ="Keyword "> open</ a > < a id ="2125 " href ="Cubical.Foundations.Pointed.Homogeneous.html " class ="Module "> Hom</ a > < a id ="2129 " class ="Keyword "> using</ a > < a id ="2135 " class ="Symbol "> (</ a > < a id ="2136 " href ="Cubical.Foundations.Pointed.Homogeneous.html#1367 " class ="Function "> isHomogeneous</ a > < a id ="2149 " class ="Symbol "> )</ a >
75+ < a id ="2051 " class ="Comment "> -- Definition 11 (version using ≡ instead of ≃⋆ is used here)</ a >
76+ < a id ="2113 " class ="Keyword "> open</ a > < a id ="2118 " href ="Cubical.Foundations.Pointed.Homogeneous.html " class ="Module "> Hom</ a > < a id ="2122 " class ="Keyword "> using</ a > < a id ="2128 " class ="Symbol "> (</ a > < a id ="2129 " href ="Cubical.Foundations.Pointed.Homogeneous.html#1367 " class ="Function "> isHomogeneous</ a > < a id ="2142 " class ="Symbol "> )</ a >
7777
78- < a id ="2152 " class ="Comment "> -- Lemma 12 (Evan's trick)</ a >
79- < a id ="2179 " class ="Keyword "> open</ a > < a id ="2184 " href ="Cubical.Foundations.Pointed.Homogeneous.html " class ="Module "> Hom</ a > < a id ="2188 " class ="Keyword "> using</ a > < a id ="2194 " class ="Symbol "> (</ a > < a id ="2195 " href ="Cubical.Foundations.Pointed.Homogeneous.html#1593 " class ="Function "> →∙Homogeneous≡</ a > < a id ="2209 " class ="Symbol "> )</ a >
78+ < a id ="2145 " class ="Comment "> -- Lemma 12 (Evan's trick)</ a >
79+ < a id ="2172 " class ="Keyword "> open</ a > < a id ="2177 " href ="Cubical.Foundations.Pointed.Homogeneous.html " class ="Module "> Hom</ a > < a id ="2181 " class ="Keyword "> using</ a > < a id ="2187 " class ="Symbol "> (</ a > < a id ="2188 " href ="Cubical.Foundations.Pointed.Homogeneous.html#1593 " class ="Function "> →∙Homogeneous≡</ a > < a id ="2202 " class ="Symbol "> )</ a >
8080
81- < a id ="2212 " class ="Comment "> -- Lemma 13 (Evan's trick for smash products)</ a >
82- < a id ="2258 " class ="Keyword "> open</ a > < a id ="2263 " href ="Cubical.HITs.SmashProduct.Base.html " class ="Module "> Smash</ a > < a id ="2269 " class ="Keyword "> using</ a > < a id ="2275 " class ="Symbol "> (</ a > < a id ="2276 " href ="Cubical.HITs.SmashProduct.Base.html#6050 " class ="Function "> ⋀→∙Homogeneous≡</ a > < a id ="2291 " class ="Symbol "> )</ a >
81+ < a id ="2205 " class ="Comment "> -- Lemma 13 (Evan's trick for smash products)</ a >
82+ < a id ="2251 " class ="Keyword "> open</ a > < a id ="2256 " href ="Cubical.HITs.SmashProduct.Base.html " class ="Module "> Smash</ a > < a id ="2262 " class ="Keyword "> using</ a > < a id ="2268 " class ="Symbol "> (</ a > < a id ="2269 " href ="Cubical.HITs.SmashProduct.Base.html#6050 " class ="Function "> ⋀→∙Homogeneous≡</ a > < a id ="2284 " class ="Symbol "> )</ a >
8383
84- < a id ="2294 " class ="Comment "> -- Lemma 14 (Evan's trick smash products, v2)</ a >
85- < a id ="2340 " class ="Keyword "> open</ a > < a id ="2345 " href ="Cubical.HITs.SmashProduct.Base.html " class ="Module "> Smash</ a > < a id ="2351 " class ="Keyword "> using</ a > < a id ="2357 " class ="Symbol "> (</ a > < a id ="2358 " href ="Cubical.HITs.SmashProduct.Base.html#6695 " class ="Function "> ⋀→Homogeneous≡</ a > < a id ="2372 " class ="Symbol "> )</ a >
84+ < a id ="2287 " class ="Comment "> -- Lemma 14 (Evan's trick smash products, v2)</ a >
85+ < a id ="2333 " class ="Keyword "> open</ a > < a id ="2338 " href ="Cubical.HITs.SmashProduct.Base.html " class ="Module "> Smash</ a > < a id ="2344 " class ="Keyword "> using</ a > < a id ="2350 " class ="Symbol "> (</ a > < a id ="2351 " href ="Cubical.HITs.SmashProduct.Base.html#6695 " class ="Function "> ⋀→Homogeneous≡</ a > < a id ="2365 " class ="Symbol "> )</ a >
8686
87- < a id ="2375 " class ="Comment "> -- Definition 15</ a >
88- < a id ="2392 " class ="Keyword "> open</ a > < a id ="2397 " href ="Cubical.HITs.SmashProduct.Base.html#37212 " class ="Module "> Smash.⋀-fun≡'</ a > < a id ="2411 " class ="Keyword "> renaming</ a > < a id ="2420 " class ="Symbol "> (</ a > < a id ="2421 " href ="Cubical.HITs.SmashProduct.Base.html#37702 " class ="Function "> Fₗ</ a > < a id ="2424 " class ="Symbol "> to</ a > < a id ="2427 " class ="Function "> L</ a > < a id ="2429 " class ="Symbol "> ;</ a > < a id ="2431 " href ="Cubical.HITs.SmashProduct.Base.html#37846 " class ="Function "> Fᵣ</ a > < a id ="2434 " class ="Symbol "> to</ a > < a id ="2437 " class ="Function "> R</ a > < a id ="2438 " class ="Symbol "> )</ a >
87+ < a id ="2368 " class ="Comment "> -- Definition 15</ a >
88+ < a id ="2385 " class ="Keyword "> open</ a > < a id ="2390 " href ="Cubical.HITs.SmashProduct.Base.html#37212 " class ="Module "> Smash.⋀-fun≡'</ a > < a id ="2404 " class ="Keyword "> renaming</ a > < a id ="2413 " class ="Symbol "> (</ a > < a id ="2414 " href ="Cubical.HITs.SmashProduct.Base.html#37702 " class ="Function "> Fₗ</ a > < a id ="2417 " class ="Symbol "> to</ a > < a id ="2420 " class ="Function "> L</ a > < a id ="2422 " class ="Symbol "> ;</ a > < a id ="2424 " href ="Cubical.HITs.SmashProduct.Base.html#37846 " class ="Function "> Fᵣ</ a > < a id ="2427 " class ="Symbol "> to</ a > < a id ="2430 " class ="Function "> R</ a > < a id ="2431 " class ="Symbol "> )</ a >
8989
90- < a id ="2441 " class ="Comment "> -- Lemma 16</ a >
91- < a id ="2453 " class ="Keyword "> open</ a > < a id ="2458 " href ="Cubical.HITs.SmashProduct.Base.html#37212 " class ="Module "> Smash.⋀-fun≡'</ a > < a id ="2472 " class ="Keyword "> using</ a > < a id ="2478 " class ="Symbol "> (</ a > < a id ="2479 " href ="Cubical.HITs.SmashProduct.Base.html#38695 " class ="Function "> main</ a > < a id ="2483 " class ="Symbol "> )</ a >
90+ < a id ="2434 " class ="Comment "> -- Lemma 16</ a >
91+ < a id ="2446 " class ="Keyword "> open</ a > < a id ="2451 " href ="Cubical.HITs.SmashProduct.Base.html#37212 " class ="Module "> Smash.⋀-fun≡'</ a > < a id ="2465 " class ="Keyword "> using</ a > < a id ="2471 " class ="Symbol "> (</ a > < a id ="2472 " href ="Cubical.HITs.SmashProduct.Base.html#38695 " class ="Function "> main</ a > < a id ="2476 " class ="Symbol "> )</ a >
9292
93- < a id ="2486 " class ="Comment "> -- Lemmas 17/18</ a >
94- < a id ="2502 " class ="Comment "> -- Omitted (used implicitly in formalisation)</ a >
93+ < a id ="2479 " class ="Comment "> -- Lemmas 17/18</ a >
94+ < a id ="2495 " class ="Comment "> -- Omitted (used implicitly in formalisation)</ a >
9595
9696
97- < a id ="2550 " class ="Comment "> ---- 5 The symmetric monoidal structure ----</ a >
98- < a id ="2595 " class ="Comment "> -- Proposition 19/20 (Hexagon and pentagon)</ a >
99- < a id ="2639 " class ="Comment "> -- Postponed - stated as part of Theorem 21</ a >
97+ < a id ="2543 " class ="Comment "> ---- 5 The symmetric monoidal structure ----</ a >
98+ < a id ="2588 " class ="Comment "> -- Proposition 19/20 (Hexagon and pentagon)</ a >
99+ < a id ="2632 " class ="Comment "> -- Postponed - stated as part of Theorem 21</ a >
100100
101- < a id ="2684 " class ="Comment "> -- Theorem 21 (Symmetric monoidal structure)</ a >
102- < a id ="2729 " class ="Keyword "> open</ a > < a id ="2734 " href ="Cubical.HITs.SmashProduct.SymmetricMonoidalCat.html " class ="Module "> SM</ a > < a id ="2737 " class ="Keyword "> using</ a > < a id ="2743 " class ="Symbol "> (</ a > < a id ="2744 " href ="Cubical.HITs.SmashProduct.SymmetricMonoidalCat.html#2498 " class ="Function "> ⋀Symm</ a > < a id ="2749 " class ="Symbol "> )</ a >
101+ < a id ="2677 " class ="Comment "> -- Theorem 21 (Symmetric monoidal structure)</ a >
102+ < a id ="2722 " class ="Keyword "> open</ a > < a id ="2727 " href ="Cubical.HITs.SmashProduct.SymmetricMonoidalCat.html " class ="Module "> SM</ a > < a id ="2730 " class ="Keyword "> using</ a > < a id ="2736 " class ="Symbol "> (</ a > < a id ="2737 " href ="Cubical.HITs.SmashProduct.SymmetricMonoidalCat.html#2498 " class ="Function "> ⋀Symm</ a > < a id ="2742 " class ="Symbol "> )</ a >
103103
104- < a id ="2752 " class ="Comment "> --- 5.1 Back to Brunerie's thesis</ a >
105- < a id ="2786 " class ="Comment "> -- This section is only meant to be an informal discussion and has not</ a >
106- < a id ="2857 " class ="Comment "> -- been formalised, as stated in the paper.</ a >
104+ < a id ="2745 " class ="Comment "> --- 5.1 Back to Brunerie's thesis</ a >
105+ < a id ="2779 " class ="Comment "> -- This section is only meant to be an informal discussion and has not</ a >
106+ < a id ="2850 " class ="Comment "> -- been formalised, as stated in the paper.</ a >
107107
108- < a id ="2902 " class ="Comment "> -- 6. A formal statement of the heuristic</ a >
109- < a id ="2944 " class ="Comment "> -- Definition 25 (FS)</ a >
110- < a id ="2966 " class ="Keyword "> open</ a > < a id ="2971 " href ="Cubical.HITs.SmashProduct.Induction.html " class ="Module "> SmashInduction</ a > < a id ="2986 " class ="Keyword "> using</ a > < a id ="2992 " class ="Symbol "> (</ a > < a id ="2993 " href ="Cubical.HITs.SmashProduct.Induction.html#1019 " class ="Function "> FS</ a > < a id ="2995 " class ="Symbol "> )</ a >
108+ < a id ="2895 " class ="Comment "> -- 6. A formal statement of the heuristic</ a >
109+ < a id ="2937 " class ="Comment "> -- Definition 25 (FS)</ a >
110+ < a id ="2959 " class ="Keyword "> open</ a > < a id ="2964 " href ="Cubical.HITs.SmashProduct.Induction.html " class ="Module "> SmashInduction</ a > < a id ="2979 " class ="Keyword "> using</ a > < a id ="2985 " class ="Symbol "> (</ a > < a id ="2986 " href ="Cubical.HITs.SmashProduct.Induction.html#1019 " class ="Function "> FS</ a > < a id ="2988 " class ="Symbol "> )</ a >
111111
112- < a id ="2998 " class ="Comment "> -- Definition 26 (⋀̃)</ a >
113- < a id ="3020 " class ="Keyword "> open</ a > < a id ="3025 " href ="Cubical.HITs.SmashProduct.Induction.html " class ="Module "> SmashInduction</ a > < a id ="3040 " class ="Keyword "> using</ a > < a id ="3046 " class ="Symbol "> (</ a > < a id ="3047 " href ="Cubical.HITs.SmashProduct.Induction.html#1441 " class ="Function "> ⋀̃</ a > < a id ="3049 " class ="Symbol "> )</ a >
112+ < a id ="2991 " class ="Comment "> -- Definition 26 (⋀̃)</ a >
113+ < a id ="3013 " class ="Keyword "> open</ a > < a id ="3018 " href ="Cubical.HITs.SmashProduct.Induction.html " class ="Module "> SmashInduction</ a > < a id ="3033 " class ="Keyword "> using</ a > < a id ="3039 " class ="Symbol "> (</ a > < a id ="3040 " href ="Cubical.HITs.SmashProduct.Induction.html#1441 " class ="Function "> ⋀̃</ a > < a id ="3042 " class ="Symbol "> )</ a >
114114
115- < a id ="3052 " class ="Comment "> -- Theorem 27 (⋀̃→⋀ induction with coherences)</ a >
116- < a id ="3099 " class ="Keyword "> open</ a > < a id ="3104 " href ="Cubical.HITs.SmashProduct.Induction.html " class ="Module "> SmashInduction</ a > < a id ="3119 " class ="Keyword "> using</ a > < a id ="3125 " class ="Symbol "> (</ a > < a id ="3126 " href ="Cubical.HITs.SmashProduct.Induction.html#3200 " class ="Function "> ⋀̃→⋀-ind</ a > < a id ="3135 " class ="Symbol "> ;</ a > < a id ="3137 " href ="Cubical.HITs.SmashProduct.Induction.html#3504 " class ="Function "> ⋀̃→⋀-ind-coh</ a > < a id ="3149 " class ="Symbol "> )</ a >
115+ < a id ="3045 " class ="Comment "> -- Theorem 27 (⋀̃→⋀ induction with coherences)</ a >
116+ < a id ="3092 " class ="Keyword "> open</ a > < a id ="3097 " href ="Cubical.HITs.SmashProduct.Induction.html " class ="Module "> SmashInduction</ a > < a id ="3112 " class ="Keyword "> using</ a > < a id ="3118 " class ="Symbol "> (</ a > < a id ="3119 " href ="Cubical.HITs.SmashProduct.Induction.html#3200 " class ="Function "> ⋀̃→⋀-ind</ a > < a id ="3128 " class ="Symbol "> ;</ a > < a id ="3130 " href ="Cubical.HITs.SmashProduct.Induction.html#3504 " class ="Function "> ⋀̃→⋀-ind-coh</ a > < a id ="3142 " class ="Symbol "> )</ a >
117117
118- < a id ="3152 " class ="Comment "> -- Corollary 28 (⋀̃→⋀ induction without)</ a >
119- < a id ="3193 " class ="Keyword "> open</ a > < a id ="3198 " href ="Cubical.HITs.SmashProduct.Induction.html " class ="Module "> SmashInduction</ a > < a id ="3213 " class ="Keyword "> using</ a > < a id ="3219 " class ="Symbol "> (</ a > < a id ="3220 " href ="Cubical.HITs.SmashProduct.Induction.html#3200 " class ="Function "> ⋀̃→⋀-ind</ a > < a id ="3228 " class ="Symbol "> )</ a >
118+ < a id ="3145 " class ="Comment "> -- Corollary 28 (⋀̃→⋀ induction without)</ a >
119+ < a id ="3186 " class ="Keyword "> open</ a > < a id ="3191 " href ="Cubical.HITs.SmashProduct.Induction.html " class ="Module "> SmashInduction</ a > < a id ="3206 " class ="Keyword "> using</ a > < a id ="3212 " class ="Symbol "> (</ a > < a id ="3213 " href ="Cubical.HITs.SmashProduct.Induction.html#3200 " class ="Function "> ⋀̃→⋀-ind</ a > < a id ="3221 " class ="Symbol "> )</ a >
120120
121- < a id ="3231 " class ="Comment "> -- Corollary 29 (⋀̃→⋀ induction for pointed maps)</ a >
122- < a id ="3281 " class ="Keyword "> open</ a > < a id ="3286 " href ="Cubical.HITs.SmashProduct.Induction.html " class ="Module "> SmashInduction</ a > < a id ="3301 " class ="Keyword "> using</ a > < a id ="3307 " class ="Symbol "> (</ a > < a id ="3308 " href ="Cubical.HITs.SmashProduct.Induction.html#6454 " class ="Function "> ⋀̃→⋀-ind∙</ a > < a id ="3317 " class ="Symbol "> )</ a >
121+ < a id ="3224 " class ="Comment "> -- Corollary 29 (⋀̃→⋀ induction for pointed maps)</ a >
122+ < a id ="3274 " class ="Keyword "> open</ a > < a id ="3279 " href ="Cubical.HITs.SmashProduct.Induction.html " class ="Module "> SmashInduction</ a > < a id ="3294 " class ="Keyword "> using</ a > < a id ="3300 " class ="Symbol "> (</ a > < a id ="3301 " href ="Cubical.HITs.SmashProduct.Induction.html#6454 " class ="Function "> ⋀̃→⋀-ind∙</ a > < a id ="3310 " class ="Symbol "> )</ a >
123123</ pre > </ body > </ html >
0 commit comments