Word choice: inductive family -> inductive types, refactor cong'

agda · Feb 8, 2019 · 43d5e90 · 43d5e90
1 parent 8da80e3
commit 43d5e90
Show file tree

Hide file tree

Showing 2 changed files with 5 additions and 4 deletions.
diff --git a/Cubical/Codata/Conat/Base.agda b/Cubical/Codata/Conat/Base.agda
@@ -8,8 +8,9 @@ This file defines:
 - Trivial operations (succ, pred) and the pattern synonyms on conaturals.
 
 While this definition can be seen as a coinductive wrapper of an inductive
-family, another way of definition is to define an inductive family that wraps
-a coinductive thunk of Nat. The standard library uses the second approach:
+datatype, another way of definition is to define an inductive datatype that
+wraps a coinductive thunk of Nat.
+The standard library uses the second approach:
 
 https://github.com/agda/agda-stdlib/blob/master/src/Codata/Conat.agda
 

diff --git a/Cubical/Core/Prelude.agda b/Cubical/Core/Prelude.agda
@@ -45,10 +45,10 @@ cong : ∀ {B : A → Set ℓ'} (f : (a : A) → B a) (p : x ≡ y)
        → PathP (λ i → B (p i)) (f x) (f y)
 cong f p = λ i → f (p i)
 
--- Non-dependent version of `cong`, to avoid some unresolved metas
+-- Less polymorphic version of `cong`, to avoid some unresolved metas
 cong′ : ∀ {B : Set ℓ'} (f : A → B) {x y : A} (p : x ≡ y)
       → Path B (f x) (f y)
-cong′ f p = λ i → f (p i)
+cong′ f = cong f
 
 -- This is called compPath and not trans in order to eliminate
 -- confusion with transp