Commits

Anonymous committed 196edfd

used ≡-reflexive definition

  • Participants
  • Parent commits d887b90

Comments (0)

Files changed (4)

           }
  
 {- В нашем мире категорий появилась первая категория. Она же - первый "объект". Теперь с помощью этого 
-   первого объекта мы начнем строить дальше -}     
+   первого объекта мы начнем строить дальше -}     

PropositionalEquivalence.agda

    open import Equivalence
    ≡-is-equivalence : IsEquivalence (_≡_ {ℓ} {A})
    ≡-is-equivalence = record
-                    { refl = ≡-refl 
+                    { refl = ≡-reflexive
                     ; sym = ≡-symmetric
                     ; trans = ≡-transitive }
 

html/Category.html

       >{- В нашем мире категорий появилась первая категория. Она же - первый "объект". Теперь с помощью этого 
    &#1087;&#1077;&#1088;&#1074;&#1086;&#1075;&#1086; &#1086;&#1073;&#1098;&#1077;&#1082;&#1090;&#1072; &#1084;&#1099; &#1085;&#1072;&#1095;&#1085;&#1077;&#1084; &#1089;&#1090;&#1088;&#1086;&#1080;&#1090;&#1100; &#1076;&#1072;&#1083;&#1100;&#1096;&#1077; -}</a
       ><a name="1675"
-      >     </a
+      >     
+</a
+      ><a name="1681" class="Comment"
+      >-- &#817;</a
       ></pre
     ></body
   ></html

html/PropositionalEquivalence.html

       >=</a
       ><a name="602"
       > </a
-      ><a name="603" href="PropositionalEquivalence.html#97" class="InductiveConstructor"
-      >&#8801;-refl</a
-      ><a name="609"
-      > 
+      ><a name="603" href="PropositionalEquivalence.html#228" class="Function"
+      >&#8801;-reflexive</a
+      ><a name="614"
+      >
                     </a
-      ><a name="631" class="Symbol"
+      ><a name="635" class="Symbol"
       >;</a
-      ><a name="632"
-      > </a
-      ><a name="633" class="Field"
-      >sym</a
       ><a name="636"
       > </a
-      ><a name="637" class="Symbol"
+      ><a name="637" class="Field"
+      >sym</a
+      ><a name="640"
+      > </a
+      ><a name="641" class="Symbol"
       >=</a
-      ><a name="638"
+      ><a name="642"
       > </a
-      ><a name="639" href="PropositionalEquivalence.html#295" class="Function"
+      ><a name="643" href="PropositionalEquivalence.html#295" class="Function"
       >&#8801;-symmetric</a
-      ><a name="650"
+      ><a name="654"
       >
                     </a
-      ><a name="671" class="Symbol"
+      ><a name="675" class="Symbol"
       >;</a
-      ><a name="672"
+      ><a name="676"
       > </a
-      ><a name="673" class="Field"
+      ><a name="677" class="Field"
       >trans</a
-      ><a name="678"
+      ><a name="682"
       > </a
-      ><a name="679" class="Symbol"
+      ><a name="683" class="Symbol"
       >=</a
-      ><a name="680"
+      ><a name="684"
       > </a
-      ><a name="681" href="PropositionalEquivalence.html#373" class="Function"
+      ><a name="685" href="PropositionalEquivalence.html#373" class="Function"
       >&#8801;-transitive</a
-      ><a name="693"
+      ><a name="697"
       > </a
-      ><a name="694" class="Symbol"
+      ><a name="698" class="Symbol"
       >}</a
-      ><a name="695"
+      ><a name="699"
       >
 
    </a
-      ><a name="700" href="PropositionalEquivalence.html#700" class="Function"
+      ><a name="704" href="PropositionalEquivalence.html#704" class="Function"
       >subst</a
-      ><a name="705"
+      ><a name="709"
       > </a
-      ><a name="706" class="Symbol"
+      ><a name="710" class="Symbol"
       >:</a
-      ><a name="707"
+      ><a name="711"
       > </a
-      ><a name="708" class="Symbol"
+      ><a name="712" class="Symbol"
       >{</a
-      ><a name="709" href="PropositionalEquivalence.html#709" class="Bound"
+      ><a name="713" href="PropositionalEquivalence.html#713" class="Bound"
       >&#8467;</a
-      ><a name="710"
+      ><a name="714"
       > </a
-      ><a name="711" class="Symbol"
+      ><a name="715" class="Symbol"
       >:</a
-      ><a name="712"
+      ><a name="716"
       > </a
-      ><a name="713" class="Symbol"
+      ><a name="717" class="Symbol"
       >_}</a
-      ><a name="715"
+      ><a name="719"
       > </a
-      ><a name="716" class="Symbol"
+      ><a name="720" class="Symbol"
       >{</a
-      ><a name="717" href="PropositionalEquivalence.html#717" class="Bound"
+      ><a name="721" href="PropositionalEquivalence.html#721" class="Bound"
       >A</a
-      ><a name="718"
+      ><a name="722"
       > </a
-      ><a name="719" class="Symbol"
+      ><a name="723" class="Symbol"
       >:</a
-      ><a name="720"
-      > </a
-      ><a name="721" class="PrimitiveType"
-      >Set</a
       ><a name="724"
       > </a
-      ><a name="725" href="PropositionalEquivalence.html#709" class="Bound"
+      ><a name="725" class="PrimitiveType"
+      >Set</a
+      ><a name="728"
+      > </a
+      ><a name="729" href="PropositionalEquivalence.html#713" class="Bound"
       >&#8467;</a
-      ><a name="726" class="Symbol"
+      ><a name="730" class="Symbol"
       >}</a
-      ><a name="727"
+      ><a name="731"
       > </a
-      ><a name="728" class="Symbol"
+      ><a name="732" class="Symbol"
       >(</a
-      ><a name="729" href="PropositionalEquivalence.html#729" class="Bound"
+      ><a name="733" href="PropositionalEquivalence.html#733" class="Bound"
       >P</a
-      ><a name="730"
-      > </a
-      ><a name="731" class="Symbol"
-      >:</a
-      ><a name="732"
-      > </a
-      ><a name="733" href="PropositionalEquivalence.html#717" class="Bound"
-      >A</a
       ><a name="734"
       > </a
       ><a name="735" class="Symbol"
-      >&#8594;</a
+      >:</a
       ><a name="736"
       > </a
-      ><a name="737" class="PrimitiveType"
-      >Set</a
+      ><a name="737" href="PropositionalEquivalence.html#721" class="Bound"
+      >A</a
+      ><a name="738"
+      > </a
+      ><a name="739" class="Symbol"
+      >&#8594;</a
       ><a name="740"
       > </a
-      ><a name="741" href="PropositionalEquivalence.html#709" class="Bound"
+      ><a name="741" class="PrimitiveType"
+      >Set</a
+      ><a name="744"
+      > </a
+      ><a name="745" href="PropositionalEquivalence.html#713" class="Bound"
       >&#8467;</a
-      ><a name="742" class="Symbol"
+      ><a name="746" class="Symbol"
       >)</a
-      ><a name="743"
+      ><a name="747"
       >  </a
-      ><a name="745" class="Symbol"
+      ><a name="749" class="Symbol"
       >{</a
-      ><a name="746" href="PropositionalEquivalence.html#746" class="Bound"
+      ><a name="750" href="PropositionalEquivalence.html#750" class="Bound"
       >a</a
-      ><a name="747"
-      > </a
-      ><a name="748" href="PropositionalEquivalence.html#748" class="Bound"
-      >b</a
-      ><a name="749"
-      > </a
-      ><a name="750" class="Symbol"
-      >:</a
       ><a name="751"
       > </a
-      ><a name="752" href="PropositionalEquivalence.html#717" class="Bound"
-      >A</a
+      ><a name="752" href="PropositionalEquivalence.html#752" class="Bound"
+      >b</a
       ><a name="753"
       > </a
       ><a name="754" class="Symbol"
-      >}</a
+      >:</a
       ><a name="755"
       > </a
-      ><a name="756" class="Symbol"
+      ><a name="756" href="PropositionalEquivalence.html#721" class="Bound"
+      >A</a
+      ><a name="757"
+      > </a
+      ><a name="758" class="Symbol"
+      >}</a
+      ><a name="759"
+      > </a
+      ><a name="760" class="Symbol"
       >(</a
-      ><a name="757" href="PropositionalEquivalence.html#757" class="Bound"
+      ><a name="761" href="PropositionalEquivalence.html#761" class="Bound"
       >a&#8801;b</a
-      ><a name="760"
-      > </a
-      ><a name="761" class="Symbol"
-      >:</a
-      ><a name="762"
-      > </a
-      ><a name="763" href="PropositionalEquivalence.html#746" class="Bound"
-      >a</a
       ><a name="764"
       > </a
-      ><a name="765" href="PropositionalEquivalence.html#45" class="Datatype Operator"
-      >&#8801;</a
+      ><a name="765" class="Symbol"
+      >:</a
       ><a name="766"
       > </a
-      ><a name="767" href="PropositionalEquivalence.html#748" class="Bound"
+      ><a name="767" href="PropositionalEquivalence.html#750" class="Bound"
+      >a</a
+      ><a name="768"
+      > </a
+      ><a name="769" href="PropositionalEquivalence.html#45" class="Datatype Operator"
+      >&#8801;</a
+      ><a name="770"
+      > </a
+      ><a name="771" href="PropositionalEquivalence.html#752" class="Bound"
       >b</a
-      ><a name="768" class="Symbol"
+      ><a name="772" class="Symbol"
       >)</a
-      ><a name="769"
-      > </a
-      ><a name="770" class="Symbol"
-      >(</a
-      ><a name="771" href="PropositionalEquivalence.html#771" class="Bound"
-      >pa</a
       ><a name="773"
       > </a
       ><a name="774" class="Symbol"
-      >:</a
-      ><a name="775"
-      > </a
-      ><a name="776" href="PropositionalEquivalence.html#729" class="Bound"
-      >P</a
+      >(</a
+      ><a name="775" href="PropositionalEquivalence.html#775" class="Bound"
+      >pa</a
       ><a name="777"
       > </a
-      ><a name="778" href="PropositionalEquivalence.html#746" class="Bound"
+      ><a name="778" class="Symbol"
+      >:</a
+      ><a name="779"
+      > </a
+      ><a name="780" href="PropositionalEquivalence.html#733" class="Bound"
+      >P</a
+      ><a name="781"
+      > </a
+      ><a name="782" href="PropositionalEquivalence.html#750" class="Bound"
       >a</a
-      ><a name="779" class="Symbol"
+      ><a name="783" class="Symbol"
       >)</a
-      ><a name="780"
-      > </a
-      ><a name="781" class="Symbol"
-      >&#8594;</a
-      ><a name="782"
-      > </a
-      ><a name="783" href="PropositionalEquivalence.html#729" class="Bound"
-      >P</a
       ><a name="784"
       > </a
-      ><a name="785" href="PropositionalEquivalence.html#748" class="Bound"
+      ><a name="785" class="Symbol"
+      >&#8594;</a
+      ><a name="786"
+      > </a
+      ><a name="787" href="PropositionalEquivalence.html#733" class="Bound"
+      >P</a
+      ><a name="788"
+      > </a
+      ><a name="789" href="PropositionalEquivalence.html#752" class="Bound"
       >b</a
-      ><a name="786"
+      ><a name="790"
       >
    </a
-      ><a name="790" href="PropositionalEquivalence.html#700" class="Function"
+      ><a name="794" href="PropositionalEquivalence.html#704" class="Function"
       >subst</a
-      ><a name="795"
+      ><a name="799"
       > </a
-      ><a name="796" href="PropositionalEquivalence.html#796" class="Bound"
+      ><a name="800" href="PropositionalEquivalence.html#800" class="Bound"
       >P</a
-      ><a name="797"
+      ><a name="801"
       > </a
-      ><a name="798" href="PropositionalEquivalence.html#97" class="InductiveConstructor"
+      ><a name="802" href="PropositionalEquivalence.html#97" class="InductiveConstructor"
       >&#8801;-refl</a
-      ><a name="804"
+      ><a name="808"
       > </a
-      ><a name="805" href="PropositionalEquivalence.html#805" class="Bound"
+      ><a name="809" href="PropositionalEquivalence.html#809" class="Bound"
       >Pa</a
-      ><a name="807"
+      ><a name="811"
       > </a
-      ><a name="808" class="Symbol"
+      ><a name="812" class="Symbol"
       >=</a
-      ><a name="809"
+      ><a name="813"
       > </a
-      ><a name="810" href="PropositionalEquivalence.html#805" class="Bound"
+      ><a name="814" href="PropositionalEquivalence.html#809" class="Bound"
       >Pa</a
-      ><a name="812"
+      ><a name="816"
       >
    
    </a