From 5907fb487732a48a31cd631ade446b5cb7034017 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Gonzalo=20Zigar=C3=A1n?= Date: Thu, 4 Apr 2024 14:45:40 -0300 Subject: [PATCH] rm md --- docs/{Clones.Basic.md => Clones.Basic.html} | 41 +++++++-------------- docs/Clones.md | 17 --------- 2 files changed, 13 insertions(+), 45 deletions(-) rename docs/{Clones.Basic.md => Clones.Basic.html} (95%) delete mode 100644 docs/Clones.md diff --git a/docs/Clones.Basic.md b/docs/Clones.Basic.html similarity index 95% rename from docs/Clones.Basic.md rename to docs/Clones.Basic.html index 2e5a0a5..cffe512 100644 --- a/docs/Clones.Basic.md +++ b/docs/Clones.Basic.html @@ -1,13 +1,4 @@ ---- -layout: default -title : "Clones.Basic module" -date : "2023-10-18" -author: "Gonzalo Zigarán" ---- - -# Clones: Basic definitions - - +

Clones: Basic definitions

module Clones.Basic where
 
 open import Agda.Primitive               using () renaming ( Set to Type )
@@ -20,10 +11,8 @@
 private variable α ρ : Level
-## Operaciones y Relaciones - -Para un conjunto $A$ y un $n ∈ ℕ$, definimos el conjunto de operaciones $n$-arias, y luego el conjunto de operaciones de aridad finita. - +

Operaciones y Relaciones

+

Para un conjunto A y un n ∈ ℕ, definimos el conjunto de operaciones n-arias, y luego el conjunto de operaciones de aridad finita.

 open import Overture        using ( Op )
 -- Operaciones de aridad finita
@@ -34,8 +23,7 @@
 FinOps A = Σ[ n ∈ ℕ ] (FinOp {n = n} A)
-De la misma manera, el conjunto de relaciones con elementos de $A$ de aridad $n$, con $n ∈ ℕ$ fijo, y de relaciones de aridad finita - +

De la misma manera, el conjunto de relaciones con elementos de A de aridad n, con n ∈ ℕ fijo, y de relaciones de aridad finita

 open import Base.Relations.Continuous    using ( Rel )
 -- Relaciones de aridad finita
@@ -46,13 +34,12 @@
 FinRels A = Σ[ n ∈ ℕ ] (FinRel {n = n} A)
-## Clones - -Difinimos a un clon de $A$ como un conjunto de operaciones en $A$ que cumple que: - -- Contiene todas las proyecciones. -- Es cerrado por composiciones. - +

Clones

+

Difinimos a un clon de A como un conjunto de operaciones en A que cumple que:

+ 
-- Funcion proyeccion, proyecta en la coordenada dada, infiere la aridad
 π : {A : Type α} → { n : ℕ } → Fin n → FinOp A
 π k = λ x → x k 
@@ -80,10 +67,8 @@
     FIsClon : isClon F
-### Clon generado - -A partir de un conjunto $F$ de operaciones en $A$ podemos hablar del clon generado por $F$ como el menor clon que contiene a $F$. Lo denotamos con [ $F$ ]. - +

Clon generado

+

A partir de un conjunto F de operaciones en A podemos hablar del clon generado por F como el menor clon que contiene a F. Lo denotamos con [ F ].

 -- clon generado
 data [_] {A : Type α} (F : Pred (FinOps A) ρ) : Pred (FinOps A) (suc Level.zero ⊔ α ⊔ ρ)
@@ -95,4 +80,4 @@
 GeneratedClonIsClon : {A : Type α} {F : Pred (FinOps A) ρ} → isClon {A = A} [ F ]
 GeneratedClonIsClon  = projections , compositions
 
-
\ No newline at end of file + diff --git a/docs/Clones.md b/docs/Clones.md deleted file mode 100644 index d73d2ca..0000000 --- a/docs/Clones.md +++ /dev/null @@ -1,17 +0,0 @@ ---- -layout: default -title : "Clones module" -date : "2023-10-18" -author: "Gonzalo Zigarán" ---- - -# Clones - - -
-module Clones where
-
-open import Clones.Basic                 public
-
-
-
\ No newline at end of file